Proof of Theorem prel12
Step | Hyp | Ref
| Expression |
1 | | preq12b.1 |
. . . . 5
⊢ 𝐴 ∈ V |
2 | 1 | prid1 3689 |
. . . 4
⊢ 𝐴 ∈ {𝐴, 𝐵} |
3 | | eleq2 2234 |
. . . 4
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} → (𝐴 ∈ {𝐴, 𝐵} ↔ 𝐴 ∈ {𝐶, 𝐷})) |
4 | 2, 3 | mpbii 147 |
. . 3
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} → 𝐴 ∈ {𝐶, 𝐷}) |
5 | | preq12b.2 |
. . . . 5
⊢ 𝐵 ∈ V |
6 | 5 | prid2 3690 |
. . . 4
⊢ 𝐵 ∈ {𝐴, 𝐵} |
7 | | eleq2 2234 |
. . . 4
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} → (𝐵 ∈ {𝐴, 𝐵} ↔ 𝐵 ∈ {𝐶, 𝐷})) |
8 | 6, 7 | mpbii 147 |
. . 3
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} → 𝐵 ∈ {𝐶, 𝐷}) |
9 | 4, 8 | jca 304 |
. 2
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} → (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷})) |
10 | 1 | elpr 3604 |
. . . 4
⊢ (𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) |
11 | | eqeq2 2180 |
. . . . . . . . . . . 12
⊢ (𝐵 = 𝐷 → (𝐴 = 𝐵 ↔ 𝐴 = 𝐷)) |
12 | 11 | notbid 662 |
. . . . . . . . . . 11
⊢ (𝐵 = 𝐷 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝐴 = 𝐷)) |
13 | | orel2 721 |
. . . . . . . . . . 11
⊢ (¬
𝐴 = 𝐷 → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) → 𝐴 = 𝐶)) |
14 | 12, 13 | syl6bi 162 |
. . . . . . . . . 10
⊢ (𝐵 = 𝐷 → (¬ 𝐴 = 𝐵 → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) → 𝐴 = 𝐶))) |
15 | 14 | com3l 81 |
. . . . . . . . 9
⊢ (¬
𝐴 = 𝐵 → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) → (𝐵 = 𝐷 → 𝐴 = 𝐶))) |
16 | 15 | imp 123 |
. . . . . . . 8
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) → (𝐵 = 𝐷 → 𝐴 = 𝐶)) |
17 | 16 | ancrd 324 |
. . . . . . 7
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) → (𝐵 = 𝐷 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) |
18 | | eqeq2 2180 |
. . . . . . . . . . . 12
⊢ (𝐵 = 𝐶 → (𝐴 = 𝐵 ↔ 𝐴 = 𝐶)) |
19 | 18 | notbid 662 |
. . . . . . . . . . 11
⊢ (𝐵 = 𝐶 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝐴 = 𝐶)) |
20 | | orel1 720 |
. . . . . . . . . . 11
⊢ (¬
𝐴 = 𝐶 → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) → 𝐴 = 𝐷)) |
21 | 19, 20 | syl6bi 162 |
. . . . . . . . . 10
⊢ (𝐵 = 𝐶 → (¬ 𝐴 = 𝐵 → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) → 𝐴 = 𝐷))) |
22 | 21 | com3l 81 |
. . . . . . . . 9
⊢ (¬
𝐴 = 𝐵 → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) → (𝐵 = 𝐶 → 𝐴 = 𝐷))) |
23 | 22 | imp 123 |
. . . . . . . 8
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) → (𝐵 = 𝐶 → 𝐴 = 𝐷)) |
24 | 23 | ancrd 324 |
. . . . . . 7
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) → (𝐵 = 𝐶 → (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))) |
25 | 17, 24 | orim12d 781 |
. . . . . 6
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) → ((𝐵 = 𝐷 ∨ 𝐵 = 𝐶) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) |
26 | 5 | elpr 3604 |
. . . . . . 7
⊢ (𝐵 ∈ {𝐶, 𝐷} ↔ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) |
27 | | orcom 723 |
. . . . . . 7
⊢ ((𝐵 = 𝐶 ∨ 𝐵 = 𝐷) ↔ (𝐵 = 𝐷 ∨ 𝐵 = 𝐶)) |
28 | 26, 27 | bitri 183 |
. . . . . 6
⊢ (𝐵 ∈ {𝐶, 𝐷} ↔ (𝐵 = 𝐷 ∨ 𝐵 = 𝐶)) |
29 | | preq12b.3 |
. . . . . . 7
⊢ 𝐶 ∈ V |
30 | | preq12b.4 |
. . . . . . 7
⊢ 𝐷 ∈ V |
31 | 1, 5, 29, 30 | preq12b 3757 |
. . . . . 6
⊢ ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))) |
32 | 25, 28, 31 | 3imtr4g 204 |
. . . . 5
⊢ ((¬
𝐴 = 𝐵 ∧ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) → (𝐵 ∈ {𝐶, 𝐷} → {𝐴, 𝐵} = {𝐶, 𝐷})) |
33 | 32 | ex 114 |
. . . 4
⊢ (¬
𝐴 = 𝐵 → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) → (𝐵 ∈ {𝐶, 𝐷} → {𝐴, 𝐵} = {𝐶, 𝐷}))) |
34 | 10, 33 | syl5bi 151 |
. . 3
⊢ (¬
𝐴 = 𝐵 → (𝐴 ∈ {𝐶, 𝐷} → (𝐵 ∈ {𝐶, 𝐷} → {𝐴, 𝐵} = {𝐶, 𝐷}))) |
35 | 34 | impd 252 |
. 2
⊢ (¬
𝐴 = 𝐵 → ((𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}) → {𝐴, 𝐵} = {𝐶, 𝐷})) |
36 | 9, 35 | impbid2 142 |
1
⊢ (¬
𝐴 = 𝐵 → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}))) |