Proof of Theorem propeqop
Step | Hyp | Ref
| Expression |
1 | | snopeqop.a |
. . . . 5
⊢ 𝐴 ∈ V |
2 | | snopeqop.b |
. . . . 5
⊢ 𝐵 ∈ V |
3 | | propeqop.e |
. . . . 5
⊢ 𝐸 ∈ V |
4 | 1, 2, 3 | opeqsn 4892 |
. . . 4
⊢
(〈𝐴, 𝐵〉 = {𝐸} ↔ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) |
5 | | snopeqop.c |
. . . . 5
⊢ 𝐶 ∈ V |
6 | | snopeqop.d |
. . . . 5
⊢ 𝐷 ∈ V |
7 | | propeqop.f |
. . . . 5
⊢ 𝐹 ∈ V |
8 | 5, 6, 3, 7 | opeqpr 4893 |
. . . 4
⊢
(〈𝐶, 𝐷〉 = {𝐸, 𝐹} ↔ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) |
9 | 4, 8 | anbi12i 729 |
. . 3
⊢
((〈𝐴, 𝐵〉 = {𝐸} ∧ 〈𝐶, 𝐷〉 = {𝐸, 𝐹}) ↔ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})))) |
10 | 1, 2, 3, 7 | opeqpr 4893 |
. . . 4
⊢
(〈𝐴, 𝐵〉 = {𝐸, 𝐹} ↔ ((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}))) |
11 | 5, 6, 3 | opeqsn 4892 |
. . . 4
⊢
(〈𝐶, 𝐷〉 = {𝐸} ↔ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})) |
12 | 10, 11 | anbi12i 729 |
. . 3
⊢
((〈𝐴, 𝐵〉 = {𝐸, 𝐹} ∧ 〈𝐶, 𝐷〉 = {𝐸}) ↔ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶}))) |
13 | 9, 12 | orbi12i 542 |
. 2
⊢
(((〈𝐴, 𝐵〉 = {𝐸} ∧ 〈𝐶, 𝐷〉 = {𝐸, 𝐹}) ∨ (〈𝐴, 𝐵〉 = {𝐸, 𝐹} ∧ 〈𝐶, 𝐷〉 = {𝐸})) ↔ (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})))) |
14 | | eqcom 2617 |
. . 3
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = 〈𝐸, 𝐹〉 ↔ 〈𝐸, 𝐹〉 = {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉}) |
15 | | opex 4859 |
. . . 4
⊢
〈𝐴, 𝐵〉 ∈ V |
16 | | opex 4859 |
. . . 4
⊢
〈𝐶, 𝐷〉 ∈ V |
17 | 3, 7, 15, 16 | opeqpr 4893 |
. . 3
⊢
(〈𝐸, 𝐹〉 = {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ↔ ((〈𝐴, 𝐵〉 = {𝐸} ∧ 〈𝐶, 𝐷〉 = {𝐸, 𝐹}) ∨ (〈𝐴, 𝐵〉 = {𝐸, 𝐹} ∧ 〈𝐶, 𝐷〉 = {𝐸}))) |
18 | 14, 17 | bitri 263 |
. 2
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = 〈𝐸, 𝐹〉 ↔ ((〈𝐴, 𝐵〉 = {𝐸} ∧ 〈𝐶, 𝐷〉 = {𝐸, 𝐹}) ∨ (〈𝐴, 𝐵〉 = {𝐸, 𝐹} ∧ 〈𝐶, 𝐷〉 = {𝐸}))) |
19 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) → 𝐴 = 𝐵) |
20 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → 𝐸 = {𝐴}) |
21 | 19, 20 | anim12i 588 |
. . . . . . . 8
⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) |
22 | | sneq 4135 |
. . . . . . . . . . . . 13
⊢ (𝐴 = 𝐶 → {𝐴} = {𝐶}) |
23 | 22 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝐴 = 𝐶 → (𝐸 = {𝐴} ↔ 𝐸 = {𝐶})) |
24 | 23 | biimpa 500 |
. . . . . . . . . . 11
⊢ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → 𝐸 = {𝐶}) |
25 | 24 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → 𝐸 = {𝐶}) |
26 | | preq1 4212 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 = 𝐶 → {𝐴, 𝐷} = {𝐶, 𝐷}) |
27 | 26 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → {𝐴, 𝐷} = {𝐶, 𝐷}) |
28 | 27 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → (𝐹 = {𝐴, 𝐷} ↔ 𝐹 = {𝐶, 𝐷})) |
29 | 28 | biimpcd 238 |
. . . . . . . . . . . 12
⊢ (𝐹 = {𝐴, 𝐷} → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → 𝐹 = {𝐶, 𝐷})) |
30 | 29 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → 𝐹 = {𝐶, 𝐷})) |
31 | 30 | imp 444 |
. . . . . . . . . 10
⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → 𝐹 = {𝐶, 𝐷}) |
32 | 25, 31 | jca 553 |
. . . . . . . . 9
⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → (𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷})) |
33 | 32 | orcd 406 |
. . . . . . . 8
⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) |
34 | 21, 33 | jca 553 |
. . . . . . 7
⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})))) |
35 | 34 | orcd 406 |
. . . . . 6
⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})))) |
36 | 35 | ex 449 |
. . . . 5
⊢ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶}))))) |
37 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) → 𝐹 = {𝐴, 𝐵}) |
38 | 20, 37 | anim12i 588 |
. . . . . . . . . 10
⊢ (((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})) → (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵})) |
39 | 38 | ancoms 468 |
. . . . . . . . 9
⊢ (((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵})) |
40 | 39 | orcd 406 |
. . . . . . . 8
⊢ (((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → ((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}))) |
41 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → 𝐴 = 𝐶) |
42 | 41 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → (𝐴 = 𝐷 ↔ 𝐶 = 𝐷)) |
43 | 42 | biimpcd 238 |
. . . . . . . . . . 11
⊢ (𝐴 = 𝐷 → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → 𝐶 = 𝐷)) |
44 | 43 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → 𝐶 = 𝐷)) |
45 | 44 | imp 444 |
. . . . . . . . 9
⊢ (((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → 𝐶 = 𝐷) |
46 | 23 | biimpd 218 |
. . . . . . . . . . . 12
⊢ (𝐴 = 𝐶 → (𝐸 = {𝐴} → 𝐸 = {𝐶})) |
47 | 46 | a1dd 48 |
. . . . . . . . . . 11
⊢ (𝐴 = 𝐶 → (𝐸 = {𝐴} → ((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) → 𝐸 = {𝐶}))) |
48 | 47 | imp 444 |
. . . . . . . . . 10
⊢ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → ((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) → 𝐸 = {𝐶})) |
49 | 48 | impcom 445 |
. . . . . . . . 9
⊢ (((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → 𝐸 = {𝐶}) |
50 | 45, 49 | jca 553 |
. . . . . . . 8
⊢ (((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})) |
51 | 40, 50 | jca 553 |
. . . . . . 7
⊢ (((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶}))) |
52 | 51 | olcd 407 |
. . . . . 6
⊢ (((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) → (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})))) |
53 | 52 | ex 449 |
. . . . 5
⊢ ((𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶}))))) |
54 | 36, 53 | jaoi 393 |
. . . 4
⊢ (((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) → (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶}))))) |
55 | 54 | impcom 445 |
. . 3
⊢ (((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))) → (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})))) |
56 | | eqeq1 2614 |
. . . . . . . . . . . . 13
⊢ (𝐸 = {𝐶} → (𝐸 = {𝐴} ↔ {𝐶} = {𝐴})) |
57 | 5 | sneqr 4311 |
. . . . . . . . . . . . . 14
⊢ ({𝐶} = {𝐴} → 𝐶 = 𝐴) |
58 | 57 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ ({𝐶} = {𝐴} → 𝐴 = 𝐶) |
59 | 56, 58 | syl6bi 242 |
. . . . . . . . . . . 12
⊢ (𝐸 = {𝐶} → (𝐸 = {𝐴} → 𝐴 = 𝐶)) |
60 | 59 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) → (𝐸 = {𝐴} → 𝐴 = 𝐶)) |
61 | | eqeq1 2614 |
. . . . . . . . . . . . 13
⊢ (𝐸 = {𝐶, 𝐷} → (𝐸 = {𝐴} ↔ {𝐶, 𝐷} = {𝐴})) |
62 | 5, 6, 1 | preqsn 4331 |
. . . . . . . . . . . . . 14
⊢ ({𝐶, 𝐷} = {𝐴} ↔ (𝐶 = 𝐷 ∧ 𝐷 = 𝐴)) |
63 | | eqtr 2629 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) → 𝐶 = 𝐴) |
64 | 63 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) → 𝐴 = 𝐶) |
65 | 62, 64 | sylbi 206 |
. . . . . . . . . . . . 13
⊢ ({𝐶, 𝐷} = {𝐴} → 𝐴 = 𝐶) |
66 | 61, 65 | syl6bi 242 |
. . . . . . . . . . . 12
⊢ (𝐸 = {𝐶, 𝐷} → (𝐸 = {𝐴} → 𝐴 = 𝐶)) |
67 | 66 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}) → (𝐸 = {𝐴} → 𝐴 = 𝐶)) |
68 | 60, 67 | jaoi 393 |
. . . . . . . . . 10
⊢ (((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) → (𝐸 = {𝐴} → 𝐴 = 𝐶)) |
69 | 68 | com12 32 |
. . . . . . . . 9
⊢ (𝐸 = {𝐴} → (((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) → 𝐴 = 𝐶)) |
70 | 69 | adantl 481 |
. . . . . . . 8
⊢ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → (((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) → 𝐴 = 𝐶)) |
71 | 70 | impcom 445 |
. . . . . . 7
⊢ ((((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → 𝐴 = 𝐶) |
72 | | simpr 476 |
. . . . . . . 8
⊢ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → 𝐸 = {𝐴}) |
73 | 72 | adantl 481 |
. . . . . . 7
⊢ ((((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → 𝐸 = {𝐴}) |
74 | 71, 73 | jca 553 |
. . . . . 6
⊢ ((((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) |
75 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → 𝐴 = 𝐵) |
76 | 75 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ (𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷})) → 𝐴 = 𝐵) |
77 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐸 = {𝐴} → (𝐸 = {𝐶} ↔ {𝐴} = {𝐶})) |
78 | 1 | sneqr 4311 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝐴} = {𝐶} → 𝐴 = 𝐶) |
79 | 78 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝐴} = {𝐶} → 𝐶 = 𝐴) |
80 | 77, 79 | syl6bi 242 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸 = {𝐴} → (𝐸 = {𝐶} → 𝐶 = 𝐴)) |
81 | 80 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → (𝐸 = {𝐶} → 𝐶 = 𝐴)) |
82 | 81 | impcom 445 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸 = {𝐶} ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → 𝐶 = 𝐴) |
83 | 82 | preq1d 4218 |
. . . . . . . . . . . . . 14
⊢ ((𝐸 = {𝐶} ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → {𝐶, 𝐷} = {𝐴, 𝐷}) |
84 | 83 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ ((𝐸 = {𝐶} ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → (𝐹 = {𝐶, 𝐷} ↔ 𝐹 = {𝐴, 𝐷})) |
85 | 84 | biimpd 218 |
. . . . . . . . . . . 12
⊢ ((𝐸 = {𝐶} ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → (𝐹 = {𝐶, 𝐷} → 𝐹 = {𝐴, 𝐷})) |
86 | 85 | impancom 455 |
. . . . . . . . . . 11
⊢ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) → ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → 𝐹 = {𝐴, 𝐷})) |
87 | 86 | impcom 445 |
. . . . . . . . . 10
⊢ (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ (𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷})) → 𝐹 = {𝐴, 𝐷}) |
88 | 76, 87 | jca 553 |
. . . . . . . . 9
⊢ (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ (𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷})) → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷})) |
89 | 88 | ex 449 |
. . . . . . . 8
⊢ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}))) |
90 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐷 = 𝐴 ↔ 𝐴 = 𝐷) |
91 | 90 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐷 = 𝐴 → 𝐴 = 𝐷) |
92 | 91 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) → 𝐴 = 𝐷) |
93 | 92 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → 𝐴 = 𝐷) |
94 | 93 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) ∧ 𝐹 = {𝐶}) → 𝐴 = 𝐷) |
95 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵) |
96 | 64 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) → (𝐴 = 𝐵 ↔ 𝐶 = 𝐵)) |
97 | 96 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → 𝐶 = 𝐵) |
98 | 97 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → 𝐵 = 𝐶) |
99 | 1, 2, 5 | preqsn 4331 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({𝐴, 𝐵} = {𝐶} ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶)) |
100 | 95, 98, 99 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → {𝐴, 𝐵} = {𝐶}) |
101 | 100 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → {𝐶} = {𝐴, 𝐵}) |
102 | 101 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → (𝐹 = {𝐶} ↔ 𝐹 = {𝐴, 𝐵})) |
103 | 102 | biimpa 500 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) ∧ 𝐹 = {𝐶}) → 𝐹 = {𝐴, 𝐵}) |
104 | 94, 103 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) ∧ 𝐹 = {𝐶}) → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})) |
105 | 104 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) ∧ 𝐴 = 𝐵) → (𝐹 = {𝐶} → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))) |
106 | 105 | ex 449 |
. . . . . . . . . . . . . . 15
⊢ ((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) → (𝐴 = 𝐵 → (𝐹 = {𝐶} → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
107 | 106 | com23 84 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 = 𝐷 ∧ 𝐷 = 𝐴) → (𝐹 = {𝐶} → (𝐴 = 𝐵 → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
108 | 62, 107 | sylbi 206 |
. . . . . . . . . . . . 13
⊢ ({𝐶, 𝐷} = {𝐴} → (𝐹 = {𝐶} → (𝐴 = 𝐵 → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
109 | 61, 108 | syl6bi 242 |
. . . . . . . . . . . 12
⊢ (𝐸 = {𝐶, 𝐷} → (𝐸 = {𝐴} → (𝐹 = {𝐶} → (𝐴 = 𝐵 → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))) |
110 | 109 | com23 84 |
. . . . . . . . . . 11
⊢ (𝐸 = {𝐶, 𝐷} → (𝐹 = {𝐶} → (𝐸 = {𝐴} → (𝐴 = 𝐵 → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))) |
111 | 110 | imp 444 |
. . . . . . . . . 10
⊢ ((𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}) → (𝐸 = {𝐴} → (𝐴 = 𝐵 → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
112 | 111 | com13 86 |
. . . . . . . . 9
⊢ (𝐴 = 𝐵 → (𝐸 = {𝐴} → ((𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}) → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
113 | 112 | imp 444 |
. . . . . . . 8
⊢ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → ((𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}) → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))) |
114 | 89, 113 | orim12d 879 |
. . . . . . 7
⊢ ((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) → (((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) → ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
115 | 114 | impcom 445 |
. . . . . 6
⊢ ((((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))) |
116 | 74, 115 | jca 553 |
. . . . 5
⊢ ((((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶})) ∧ (𝐴 = 𝐵 ∧ 𝐸 = {𝐴})) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
117 | 116 | ancoms 468 |
. . . 4
⊢ (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
118 | | eqeq1 2614 |
. . . . . . . . . . . . . . . 16
⊢ (𝐸 = {𝐶} → (𝐸 = {𝐴, 𝐵} ↔ {𝐶} = {𝐴, 𝐵})) |
119 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝐶} = {𝐴, 𝐵} ↔ {𝐴, 𝐵} = {𝐶}) |
120 | 119, 99 | bitri 263 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝐶} = {𝐴, 𝐵} ↔ (𝐴 = 𝐵 ∧ 𝐵 = 𝐶)) |
121 | | eqtr 2629 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶) |
122 | 121 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐸 = {𝐶}) → 𝐴 = 𝐶) |
123 | 121 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐶 = 𝐴) |
124 | | sneq 4135 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐶 = 𝐴 → {𝐶} = {𝐴}) |
125 | 123, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → {𝐶} = {𝐴}) |
126 | 125 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐸 = {𝐶} ↔ 𝐸 = {𝐴})) |
127 | 126 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐸 = {𝐶}) → 𝐸 = {𝐴}) |
128 | 122, 127 | jca 553 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐸 = {𝐶}) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) |
129 | 128 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐸 = {𝐶} → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))) |
130 | 129 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐹 = {𝐴} → (𝐸 = {𝐶} → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})))) |
131 | 130 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐶 = 𝐷 → ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐹 = {𝐴} → (𝐸 = {𝐶} → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))))) |
132 | 131 | com14 94 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐸 = {𝐶} → ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐹 = {𝐴} → (𝐶 = 𝐷 → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))))) |
133 | 120, 132 | syl5bi 231 |
. . . . . . . . . . . . . . . 16
⊢ (𝐸 = {𝐶} → ({𝐶} = {𝐴, 𝐵} → (𝐹 = {𝐴} → (𝐶 = 𝐷 → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))))) |
134 | 118, 133 | sylbid 229 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 = {𝐶} → (𝐸 = {𝐴, 𝐵} → (𝐹 = {𝐴} → (𝐶 = 𝐷 → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))))) |
135 | 134 | com24 93 |
. . . . . . . . . . . . . 14
⊢ (𝐸 = {𝐶} → (𝐶 = 𝐷 → (𝐹 = {𝐴} → (𝐸 = {𝐴, 𝐵} → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))))) |
136 | 135 | impcom 445 |
. . . . . . . . . . . . 13
⊢ ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (𝐹 = {𝐴} → (𝐸 = {𝐴, 𝐵} → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})))) |
137 | 136 | com13 86 |
. . . . . . . . . . . 12
⊢ (𝐸 = {𝐴, 𝐵} → (𝐹 = {𝐴} → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})))) |
138 | 137 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))) |
139 | 59 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (𝐸 = {𝐴} → 𝐴 = 𝐶)) |
140 | 139 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 = {𝐴} → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → 𝐴 = 𝐶)) |
141 | 140 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → 𝐴 = 𝐶)) |
142 | 141 | imp 444 |
. . . . . . . . . . . . 13
⊢ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})) → 𝐴 = 𝐶) |
143 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) → 𝐸 = {𝐴}) |
144 | 143 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})) → 𝐸 = {𝐴}) |
145 | 142, 144 | jca 553 |
. . . . . . . . . . . 12
⊢ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) |
146 | 145 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))) |
147 | 138, 146 | jaoi 393 |
. . . . . . . . . 10
⊢ (((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) ∨ (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵})) → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴}))) |
148 | 147 | impcom 445 |
. . . . . . . . 9
⊢ (((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) ∧ ((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) ∨ (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}))) → (𝐴 = 𝐶 ∧ 𝐸 = {𝐴})) |
149 | | eqeq1 2614 |
. . . . . . . . . . . . . . . 16
⊢ (𝐸 = {𝐴, 𝐵} → (𝐸 = {𝐶} ↔ {𝐴, 𝐵} = {𝐶})) |
150 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵) |
151 | 150 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐶 = 𝐷) → 𝐴 = 𝐵) |
152 | 151 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐶 = 𝐷) ∧ 𝐹 = {𝐴}) → 𝐴 = 𝐵) |
153 | | eqtr 2629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 = 𝐶 ∧ 𝐶 = 𝐷) → 𝐴 = 𝐷) |
154 | | dfsn2 4138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ {𝐴} = {𝐴, 𝐴} |
155 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐴 = 𝐷 → {𝐴, 𝐴} = {𝐴, 𝐷}) |
156 | 154, 155 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐴 = 𝐷 → {𝐴} = {𝐴, 𝐷}) |
157 | 153, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 = 𝐶 ∧ 𝐶 = 𝐷) → {𝐴} = {𝐴, 𝐷}) |
158 | 157 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐴 = 𝐶 → (𝐶 = 𝐷 → {𝐴} = {𝐴, 𝐷})) |
159 | 121, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐶 = 𝐷 → {𝐴} = {𝐴, 𝐷})) |
160 | 159 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐶 = 𝐷) → {𝐴} = {𝐴, 𝐷}) |
161 | 160 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐶 = 𝐷) → (𝐹 = {𝐴} ↔ 𝐹 = {𝐴, 𝐷})) |
162 | 161 | biimpa 500 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐶 = 𝐷) ∧ 𝐹 = {𝐴}) → 𝐹 = {𝐴, 𝐷}) |
163 | 152, 162 | jca 553 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐶 = 𝐷) ∧ 𝐹 = {𝐴}) → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷})) |
164 | 163 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) ∧ 𝐶 = 𝐷) → (𝐹 = {𝐴} → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}))) |
165 | 164 | ex 449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐶 = 𝐷 → (𝐹 = {𝐴} → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷})))) |
166 | 165 | com23 84 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → (𝐹 = {𝐴} → (𝐶 = 𝐷 → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷})))) |
167 | 99, 166 | sylbi 206 |
. . . . . . . . . . . . . . . 16
⊢ ({𝐴, 𝐵} = {𝐶} → (𝐹 = {𝐴} → (𝐶 = 𝐷 → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷})))) |
168 | 149, 167 | syl6bi 242 |
. . . . . . . . . . . . . . 15
⊢ (𝐸 = {𝐴, 𝐵} → (𝐸 = {𝐶} → (𝐹 = {𝐴} → (𝐶 = 𝐷 → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}))))) |
169 | 168 | com23 84 |
. . . . . . . . . . . . . 14
⊢ (𝐸 = {𝐴, 𝐵} → (𝐹 = {𝐴} → (𝐸 = {𝐶} → (𝐶 = 𝐷 → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}))))) |
170 | 169 | imp 444 |
. . . . . . . . . . . . 13
⊢ ((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) → (𝐸 = {𝐶} → (𝐶 = 𝐷 → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷})))) |
171 | 170 | com13 86 |
. . . . . . . . . . . 12
⊢ (𝐶 = 𝐷 → (𝐸 = {𝐶} → ((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷})))) |
172 | 171 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → ((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) → (𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}))) |
173 | 80 | imp 444 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐸 = {𝐴} ∧ 𝐸 = {𝐶}) → 𝐶 = 𝐴) |
174 | 173 | eqeq1d 2612 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸 = {𝐴} ∧ 𝐸 = {𝐶}) → (𝐶 = 𝐷 ↔ 𝐴 = 𝐷)) |
175 | 174 | biimpd 218 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸 = {𝐴} ∧ 𝐸 = {𝐶}) → (𝐶 = 𝐷 → 𝐴 = 𝐷)) |
176 | 175 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝐸 = {𝐴} → (𝐸 = {𝐶} → (𝐶 = 𝐷 → 𝐴 = 𝐷))) |
177 | 176 | com13 86 |
. . . . . . . . . . . . 13
⊢ (𝐶 = 𝐷 → (𝐸 = {𝐶} → (𝐸 = {𝐴} → 𝐴 = 𝐷))) |
178 | 177 | imp 444 |
. . . . . . . . . . . 12
⊢ ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (𝐸 = {𝐴} → 𝐴 = 𝐷)) |
179 | 178 | anim1d 586 |
. . . . . . . . . . 11
⊢ ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → ((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) → (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))) |
180 | 172, 179 | orim12d 879 |
. . . . . . . . . 10
⊢ ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) ∨ (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵})) → ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
181 | 180 | imp 444 |
. . . . . . . . 9
⊢ (((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) ∧ ((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) ∨ (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}))) → ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))) |
182 | 148, 181 | jca 553 |
. . . . . . . 8
⊢ (((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) ∧ ((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) ∨ (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}))) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
183 | 182 | ex 449 |
. . . . . . 7
⊢ ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → (((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) ∨ (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵})) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))) |
184 | 183 | com12 32 |
. . . . . 6
⊢ (((𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴}) ∨ (𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵})) → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))) |
185 | 184 | orcoms 403 |
. . . . 5
⊢ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) → ((𝐶 = 𝐷 ∧ 𝐸 = {𝐶}) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))))) |
186 | 185 | imp 444 |
. . . 4
⊢ ((((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
187 | 117, 186 | jaoi 393 |
. . 3
⊢ ((((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶}))) → ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |
188 | 55, 187 | impbii 198 |
. 2
⊢ (((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵}))) ↔ (((𝐴 = 𝐵 ∧ 𝐸 = {𝐴}) ∧ ((𝐸 = {𝐶} ∧ 𝐹 = {𝐶, 𝐷}) ∨ (𝐸 = {𝐶, 𝐷} ∧ 𝐹 = {𝐶}))) ∨ (((𝐸 = {𝐴} ∧ 𝐹 = {𝐴, 𝐵}) ∨ (𝐸 = {𝐴, 𝐵} ∧ 𝐹 = {𝐴})) ∧ (𝐶 = 𝐷 ∧ 𝐸 = {𝐶})))) |
189 | 13, 18, 188 | 3bitr4i 291 |
1
⊢
({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = 〈𝐸, 𝐹〉 ↔ ((𝐴 = 𝐶 ∧ 𝐸 = {𝐴}) ∧ ((𝐴 = 𝐵 ∧ 𝐹 = {𝐴, 𝐷}) ∨ (𝐴 = 𝐷 ∧ 𝐹 = {𝐴, 𝐵})))) |