Proof of Theorem preq12b
Step | Hyp | Ref
| Expression |
1 | | preq12b.1 |
. . . . . 6
⊢ A ∈
V |
2 | 1 | prid1 3467 |
. . . . 5
⊢ A ∈ {A, B} |
3 | | eleq2 2098 |
. . . . 5
⊢
({A, B} = {𝐶, 𝐷} → (A ∈ {A, B} ↔
A ∈
{𝐶, 𝐷})) |
4 | 2, 3 | mpbii 136 |
. . . 4
⊢
({A, B} = {𝐶, 𝐷} → A ∈ {𝐶, 𝐷}) |
5 | 1 | elpr 3385 |
. . . 4
⊢ (A ∈ {𝐶, 𝐷} ↔ (A = 𝐶 ∨ A = 𝐷)) |
6 | 4, 5 | sylib 127 |
. . 3
⊢
({A, B} = {𝐶, 𝐷} → (A = 𝐶 ∨ A = 𝐷)) |
7 | | preq1 3438 |
. . . . . . . 8
⊢ (A = 𝐶 → {A, B} = {𝐶, B}) |
8 | 7 | eqeq1d 2045 |
. . . . . . 7
⊢ (A = 𝐶 → ({A, B} = {𝐶, 𝐷} ↔ {𝐶, B} =
{𝐶, 𝐷})) |
9 | | preq12b.2 |
. . . . . . . 8
⊢ B ∈
V |
10 | | preq12b.4 |
. . . . . . . 8
⊢ 𝐷 ∈ V |
11 | 9, 10 | preqr2 3531 |
. . . . . . 7
⊢ ({𝐶, B} = {𝐶, 𝐷} → B = 𝐷) |
12 | 8, 11 | syl6bi 152 |
. . . . . 6
⊢ (A = 𝐶 → ({A, B} = {𝐶, 𝐷} → B = 𝐷)) |
13 | 12 | com12 27 |
. . . . 5
⊢
({A, B} = {𝐶, 𝐷} → (A = 𝐶 → B = 𝐷)) |
14 | 13 | ancld 308 |
. . . 4
⊢
({A, B} = {𝐶, 𝐷} → (A = 𝐶 → (A = 𝐶 ∧ B = 𝐷))) |
15 | | prcom 3437 |
. . . . . . 7
⊢ {𝐶, 𝐷} = {𝐷, 𝐶} |
16 | 15 | eqeq2i 2047 |
. . . . . 6
⊢
({A, B} = {𝐶, 𝐷} ↔ {A, B} = {𝐷, 𝐶}) |
17 | | preq1 3438 |
. . . . . . . . 9
⊢ (A = 𝐷 → {A, B} = {𝐷, B}) |
18 | 17 | eqeq1d 2045 |
. . . . . . . 8
⊢ (A = 𝐷 → ({A, B} = {𝐷, 𝐶} ↔ {𝐷, B} =
{𝐷, 𝐶})) |
19 | | preq12b.3 |
. . . . . . . . 9
⊢ 𝐶 ∈ V |
20 | 9, 19 | preqr2 3531 |
. . . . . . . 8
⊢ ({𝐷, B} = {𝐷, 𝐶} → B = 𝐶) |
21 | 18, 20 | syl6bi 152 |
. . . . . . 7
⊢ (A = 𝐷 → ({A, B} = {𝐷, 𝐶} → B = 𝐶)) |
22 | 21 | com12 27 |
. . . . . 6
⊢
({A, B} = {𝐷, 𝐶} → (A = 𝐷 → B = 𝐶)) |
23 | 16, 22 | sylbi 114 |
. . . . 5
⊢
({A, B} = {𝐶, 𝐷} → (A = 𝐷 → B = 𝐶)) |
24 | 23 | ancld 308 |
. . . 4
⊢
({A, B} = {𝐶, 𝐷} → (A = 𝐷 → (A = 𝐷 ∧ B = 𝐶))) |
25 | 14, 24 | orim12d 699 |
. . 3
⊢
({A, B} = {𝐶, 𝐷} → ((A = 𝐶 ∨ A = 𝐷) → ((A = 𝐶 ∧ B = 𝐷) ∨
(A = 𝐷 ∧ B = 𝐶)))) |
26 | 6, 25 | mpd 13 |
. 2
⊢
({A, B} = {𝐶, 𝐷} → ((A = 𝐶 ∧ B = 𝐷) ∨
(A = 𝐷 ∧ B = 𝐶))) |
27 | | preq12 3440 |
. . 3
⊢
((A = 𝐶 ∧ B = 𝐷) → {A, B} = {𝐶, 𝐷}) |
28 | | prcom 3437 |
. . . . 5
⊢ {𝐷, B} = {B, 𝐷} |
29 | 17, 28 | syl6eq 2085 |
. . . 4
⊢ (A = 𝐷 → {A, B} =
{B, 𝐷}) |
30 | | preq1 3438 |
. . . 4
⊢ (B = 𝐶 → {B, 𝐷} = {𝐶, 𝐷}) |
31 | 29, 30 | sylan9eq 2089 |
. . 3
⊢
((A = 𝐷 ∧ B = 𝐶) → {A, B} = {𝐶, 𝐷}) |
32 | 27, 31 | jaoi 635 |
. 2
⊢
(((A = 𝐶 ∧ B = 𝐷) ∨
(A = 𝐷 ∧ B = 𝐶)) → {A, B} = {𝐶, 𝐷}) |
33 | 26, 32 | impbii 117 |
1
⊢
({A, B} = {𝐶, 𝐷} ↔ ((A = 𝐶 ∧ B = 𝐷) ∨
(A = 𝐷 ∧ B = 𝐶))) |