Proof of Theorem prel12
Step | Hyp | Ref
| Expression |
1 | | preq12b.1 |
. . . . 5
⊢ A ∈
V |
2 | 1 | prid1 3467 |
. . . 4
⊢ A ∈ {A, B} |
3 | | eleq2 2098 |
. . . 4
⊢
({A, B} = {𝐶, 𝐷} → (A ∈ {A, B} ↔
A ∈
{𝐶, 𝐷})) |
4 | 2, 3 | mpbii 136 |
. . 3
⊢
({A, B} = {𝐶, 𝐷} → A ∈ {𝐶, 𝐷}) |
5 | | preq12b.2 |
. . . . 5
⊢ B ∈
V |
6 | 5 | prid2 3468 |
. . . 4
⊢ B ∈ {A, B} |
7 | | eleq2 2098 |
. . . 4
⊢
({A, B} = {𝐶, 𝐷} → (B ∈ {A, B} ↔
B ∈
{𝐶, 𝐷})) |
8 | 6, 7 | mpbii 136 |
. . 3
⊢
({A, B} = {𝐶, 𝐷} → B ∈ {𝐶, 𝐷}) |
9 | 4, 8 | jca 290 |
. 2
⊢
({A, B} = {𝐶, 𝐷} → (A ∈ {𝐶, 𝐷} ∧
B ∈
{𝐶, 𝐷})) |
10 | 1 | elpr 3385 |
. . . 4
⊢ (A ∈ {𝐶, 𝐷} ↔ (A = 𝐶 ∨ A = 𝐷)) |
11 | | eqeq2 2046 |
. . . . . . . . . . . 12
⊢ (B = 𝐷 → (A = B ↔
A = 𝐷)) |
12 | 11 | notbid 591 |
. . . . . . . . . . 11
⊢ (B = 𝐷 → (¬ A = B ↔
¬ A = 𝐷)) |
13 | | orel2 644 |
. . . . . . . . . . 11
⊢ (¬
A = 𝐷 → ((A = 𝐶 ∨ A = 𝐷) → A = 𝐶)) |
14 | 12, 13 | syl6bi 152 |
. . . . . . . . . 10
⊢ (B = 𝐷 → (¬ A = B →
((A = 𝐶 ∨ A = 𝐷) → A = 𝐶))) |
15 | 14 | com3l 75 |
. . . . . . . . 9
⊢ (¬
A = B
→ ((A = 𝐶 ∨ A = 𝐷) → (B = 𝐷 → A = 𝐶))) |
16 | 15 | imp 115 |
. . . . . . . 8
⊢ ((¬
A = B
∧ (A =
𝐶
∨ A = 𝐷)) → (B = 𝐷 → A = 𝐶)) |
17 | 16 | ancrd 309 |
. . . . . . 7
⊢ ((¬
A = B
∧ (A =
𝐶
∨ A = 𝐷)) → (B = 𝐷 → (A = 𝐶 ∧ B = 𝐷))) |
18 | | eqeq2 2046 |
. . . . . . . . . . . 12
⊢ (B = 𝐶 → (A = B ↔
A = 𝐶)) |
19 | 18 | notbid 591 |
. . . . . . . . . . 11
⊢ (B = 𝐶 → (¬ A = B ↔
¬ A = 𝐶)) |
20 | | orel1 643 |
. . . . . . . . . . 11
⊢ (¬
A = 𝐶 → ((A = 𝐶 ∨ A = 𝐷) → A = 𝐷)) |
21 | 19, 20 | syl6bi 152 |
. . . . . . . . . 10
⊢ (B = 𝐶 → (¬ A = B →
((A = 𝐶 ∨ A = 𝐷) → A = 𝐷))) |
22 | 21 | com3l 75 |
. . . . . . . . 9
⊢ (¬
A = B
→ ((A = 𝐶 ∨ A = 𝐷) → (B = 𝐶 → A = 𝐷))) |
23 | 22 | imp 115 |
. . . . . . . 8
⊢ ((¬
A = B
∧ (A =
𝐶
∨ A = 𝐷)) → (B = 𝐶 → A = 𝐷)) |
24 | 23 | ancrd 309 |
. . . . . . 7
⊢ ((¬
A = B
∧ (A =
𝐶
∨ A = 𝐷)) → (B = 𝐶 → (A = 𝐷 ∧ B = 𝐶))) |
25 | 17, 24 | orim12d 699 |
. . . . . 6
⊢ ((¬
A = B
∧ (A =
𝐶
∨ A = 𝐷)) → ((B = 𝐷 ∨ B = 𝐶) → ((A = 𝐶 ∧ B = 𝐷) ∨
(A = 𝐷 ∧ B = 𝐶)))) |
26 | 5 | elpr 3385 |
. . . . . . 7
⊢ (B ∈ {𝐶, 𝐷} ↔ (B = 𝐶 ∨ B = 𝐷)) |
27 | | orcom 646 |
. . . . . . 7
⊢
((B = 𝐶 ∨ B = 𝐷) ↔ (B = 𝐷 ∨ B = 𝐶)) |
28 | 26, 27 | bitri 173 |
. . . . . 6
⊢ (B ∈ {𝐶, 𝐷} ↔ (B = 𝐷 ∨ B = 𝐶)) |
29 | | preq12b.3 |
. . . . . . 7
⊢ 𝐶 ∈ V |
30 | | preq12b.4 |
. . . . . . 7
⊢ 𝐷 ∈ V |
31 | 1, 5, 29, 30 | preq12b 3532 |
. . . . . 6
⊢
({A, B} = {𝐶, 𝐷} ↔ ((A = 𝐶 ∧ B = 𝐷) ∨
(A = 𝐷 ∧ B = 𝐶))) |
32 | 25, 28, 31 | 3imtr4g 194 |
. . . . 5
⊢ ((¬
A = B
∧ (A =
𝐶
∨ A = 𝐷)) → (B ∈ {𝐶, 𝐷} → {A, B} = {𝐶, 𝐷})) |
33 | 32 | ex 108 |
. . . 4
⊢ (¬
A = B
→ ((A = 𝐶 ∨ A = 𝐷) → (B ∈ {𝐶, 𝐷} → {A, B} = {𝐶, 𝐷}))) |
34 | 10, 33 | syl5bi 141 |
. . 3
⊢ (¬
A = B
→ (A ∈ {𝐶, 𝐷} → (B ∈ {𝐶, 𝐷} → {A, B} = {𝐶, 𝐷}))) |
35 | 34 | impd 242 |
. 2
⊢ (¬
A = B
→ ((A ∈ {𝐶, 𝐷} ∧
B ∈
{𝐶, 𝐷}) → {A, B} = {𝐶, 𝐷})) |
36 | 9, 35 | impbid2 131 |
1
⊢ (¬
A = B
→ ({A, B} = {𝐶, 𝐷} ↔ (A ∈ {𝐶, 𝐷} ∧
B ∈
{𝐶, 𝐷}))) |