Step | Hyp | Ref
| Expression |
1 | | prop 6458 |
. . . . . . . . 9
⊢ (B ∈
P → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
2 | | elprnql 6464 |
. . . . . . . . 9
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ y ∈ (1st ‘B)) → y
∈ Q) |
3 | 1, 2 | sylan 267 |
. . . . . . . 8
⊢
((B ∈ P ∧ y ∈ (1st ‘B)) → y
∈ Q) |
4 | | prop 6458 |
. . . . . . . . . . . . 13
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
5 | | elprnql 6464 |
. . . . . . . . . . . . 13
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ z ∈ (1st ‘A)) → z
∈ Q) |
6 | 4, 5 | sylan 267 |
. . . . . . . . . . . 12
⊢
((A ∈ P ∧ z ∈ (1st ‘A)) → z
∈ Q) |
7 | | addcomnqg 6365 |
. . . . . . . . . . . . 13
⊢
((y ∈ Q ∧ z ∈ Q) → (y +Q z) = (z
+Q y)) |
8 | 7 | eqeq2d 2048 |
. . . . . . . . . . . 12
⊢
((y ∈ Q ∧ z ∈ Q) → (x = (y
+Q z) ↔
x = (z
+Q y))) |
9 | 6, 8 | sylan2 270 |
. . . . . . . . . . 11
⊢
((y ∈ Q ∧ (A ∈ P ∧ z ∈ (1st ‘A))) → (x =
(y +Q z) ↔ x =
(z +Q y))) |
10 | 9 | anassrs 380 |
. . . . . . . . . 10
⊢
(((y ∈ Q ∧ A ∈ P) ∧ z ∈ (1st ‘A)) → (x =
(y +Q z) ↔ x =
(z +Q y))) |
11 | 10 | rexbidva 2317 |
. . . . . . . . 9
⊢
((y ∈ Q ∧ A ∈ P) → (∃z ∈ (1st ‘A)x = (y +Q z) ↔ ∃z ∈ (1st ‘A)x = (z +Q y))) |
12 | 11 | ancoms 255 |
. . . . . . . 8
⊢
((A ∈ P ∧ y ∈ Q) → (∃z ∈ (1st ‘A)x = (y +Q z) ↔ ∃z ∈ (1st ‘A)x = (z +Q y))) |
13 | 3, 12 | sylan2 270 |
. . . . . . 7
⊢
((A ∈ P ∧ (B ∈ P ∧ y ∈ (1st ‘B))) → (∃z ∈ (1st ‘A)x = (y +Q z) ↔ ∃z ∈ (1st ‘A)x = (z +Q y))) |
14 | 13 | anassrs 380 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P) ∧ y ∈ (1st ‘B)) → (∃z ∈ (1st ‘A)x = (y +Q z) ↔ ∃z ∈ (1st ‘A)x = (z +Q y))) |
15 | 14 | rexbidva 2317 |
. . . . 5
⊢
((A ∈ P ∧ B ∈ P) → (∃y ∈ (1st ‘B)∃z ∈
(1st ‘A)x = (y
+Q z) ↔ ∃y ∈ (1st ‘B)∃z ∈
(1st ‘A)x = (z
+Q y))) |
16 | | rexcom 2468 |
. . . . 5
⊢ (∃y ∈ (1st ‘B)∃z ∈
(1st ‘A)x = (z
+Q y) ↔ ∃z ∈ (1st ‘A)∃y ∈
(1st ‘B)x = (z
+Q y)) |
17 | 15, 16 | syl6bb 185 |
. . . 4
⊢
((A ∈ P ∧ B ∈ P) → (∃y ∈ (1st ‘B)∃z ∈
(1st ‘A)x = (y
+Q z) ↔ ∃z ∈ (1st ‘A)∃y ∈
(1st ‘B)x = (z
+Q y))) |
18 | 17 | rabbidv 2543 |
. . 3
⊢
((A ∈ P ∧ B ∈ P) → {x ∈
Q ∣ ∃y ∈
(1st ‘B)∃z ∈ (1st ‘A)x = (y +Q z)} = {x ∈ Q ∣ ∃z ∈ (1st ‘A)∃y ∈
(1st ‘B)x = (z
+Q y)}) |
19 | | elprnqu 6465 |
. . . . . . . . 9
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ y ∈ (2nd ‘B)) → y
∈ Q) |
20 | 1, 19 | sylan 267 |
. . . . . . . 8
⊢
((B ∈ P ∧ y ∈ (2nd ‘B)) → y
∈ Q) |
21 | | elprnqu 6465 |
. . . . . . . . . . . . 13
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ z ∈ (2nd ‘A)) → z
∈ Q) |
22 | 4, 21 | sylan 267 |
. . . . . . . . . . . 12
⊢
((A ∈ P ∧ z ∈ (2nd ‘A)) → z
∈ Q) |
23 | 22, 8 | sylan2 270 |
. . . . . . . . . . 11
⊢
((y ∈ Q ∧ (A ∈ P ∧ z ∈ (2nd ‘A))) → (x =
(y +Q z) ↔ x =
(z +Q y))) |
24 | 23 | anassrs 380 |
. . . . . . . . . 10
⊢
(((y ∈ Q ∧ A ∈ P) ∧ z ∈ (2nd ‘A)) → (x =
(y +Q z) ↔ x =
(z +Q y))) |
25 | 24 | rexbidva 2317 |
. . . . . . . . 9
⊢
((y ∈ Q ∧ A ∈ P) → (∃z ∈ (2nd ‘A)x = (y +Q z) ↔ ∃z ∈ (2nd ‘A)x = (z +Q y))) |
26 | 25 | ancoms 255 |
. . . . . . . 8
⊢
((A ∈ P ∧ y ∈ Q) → (∃z ∈ (2nd ‘A)x = (y +Q z) ↔ ∃z ∈ (2nd ‘A)x = (z +Q y))) |
27 | 20, 26 | sylan2 270 |
. . . . . . 7
⊢
((A ∈ P ∧ (B ∈ P ∧ y ∈ (2nd ‘B))) → (∃z ∈ (2nd ‘A)x = (y +Q z) ↔ ∃z ∈ (2nd ‘A)x = (z +Q y))) |
28 | 27 | anassrs 380 |
. . . . . 6
⊢
(((A ∈ P ∧ B ∈ P) ∧ y ∈ (2nd ‘B)) → (∃z ∈ (2nd ‘A)x = (y +Q z) ↔ ∃z ∈ (2nd ‘A)x = (z +Q y))) |
29 | 28 | rexbidva 2317 |
. . . . 5
⊢
((A ∈ P ∧ B ∈ P) → (∃y ∈ (2nd ‘B)∃z ∈
(2nd ‘A)x = (y
+Q z) ↔ ∃y ∈ (2nd ‘B)∃z ∈
(2nd ‘A)x = (z
+Q y))) |
30 | | rexcom 2468 |
. . . . 5
⊢ (∃y ∈ (2nd ‘B)∃z ∈
(2nd ‘A)x = (z
+Q y) ↔ ∃z ∈ (2nd ‘A)∃y ∈
(2nd ‘B)x = (z
+Q y)) |
31 | 29, 30 | syl6bb 185 |
. . . 4
⊢
((A ∈ P ∧ B ∈ P) → (∃y ∈ (2nd ‘B)∃z ∈
(2nd ‘A)x = (y
+Q z) ↔ ∃z ∈ (2nd ‘A)∃y ∈
(2nd ‘B)x = (z
+Q y))) |
32 | 31 | rabbidv 2543 |
. . 3
⊢
((A ∈ P ∧ B ∈ P) → {x ∈
Q ∣ ∃y ∈
(2nd ‘B)∃z ∈ (2nd ‘A)x = (y +Q z)} = {x ∈ Q ∣ ∃z ∈ (2nd ‘A)∃y ∈
(2nd ‘B)x = (z
+Q y)}) |
33 | 18, 32 | opeq12d 3548 |
. 2
⊢
((A ∈ P ∧ B ∈ P) → 〈{x ∈
Q ∣ ∃y ∈
(1st ‘B)∃z ∈ (1st ‘A)x = (y +Q z)}, {x ∈ Q ∣ ∃y ∈ (2nd ‘B)∃z ∈
(2nd ‘A)x = (y
+Q z)}〉 =
〈{x ∈ Q ∣ ∃z ∈ (1st ‘A)∃y ∈
(1st ‘B)x = (z
+Q y)}, {x ∈
Q ∣ ∃z ∈
(2nd ‘A)∃y ∈ (2nd ‘B)x = (z +Q y)}〉) |
34 | | plpvlu 6521 |
. . 3
⊢
((B ∈ P ∧ A ∈ P) → (B +P A) = 〈{x
∈ Q ∣ ∃y ∈ (1st ‘B)∃z ∈
(1st ‘A)x = (y
+Q z)}, {x ∈
Q ∣ ∃y ∈
(2nd ‘B)∃z ∈ (2nd ‘A)x = (y +Q z)}〉) |
35 | 34 | ancoms 255 |
. 2
⊢
((A ∈ P ∧ B ∈ P) → (B +P A) = 〈{x
∈ Q ∣ ∃y ∈ (1st ‘B)∃z ∈
(1st ‘A)x = (y
+Q z)}, {x ∈
Q ∣ ∃y ∈
(2nd ‘B)∃z ∈ (2nd ‘A)x = (y +Q z)}〉) |
36 | | plpvlu 6521 |
. 2
⊢
((A ∈ P ∧ B ∈ P) → (A +P B) = 〈{x
∈ Q ∣ ∃z ∈ (1st ‘A)∃y ∈
(1st ‘B)x = (z
+Q y)}, {x ∈
Q ∣ ∃z ∈
(2nd ‘A)∃y ∈ (2nd ‘B)x = (z +Q y)}〉) |
37 | 33, 35, 36 | 3eqtr4rd 2080 |
1
⊢
((A ∈ P ∧ B ∈ P) → (A +P B) = (B
+P A)) |