Proof of Theorem prel12g
| Step | Hyp | Ref
| Expression |
| 1 | | preq12nebg 4863 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) |
| 2 | | prid1g 4760 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴, 𝐷}) |
| 3 | 2 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ {𝐴, 𝐷}) |
| 4 | 3 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 = 𝐶) → 𝐴 ∈ {𝐴, 𝐷}) |
| 5 | | preq1 4733 |
. . . . . . . 8
⊢ (𝐴 = 𝐶 → {𝐴, 𝐷} = {𝐶, 𝐷}) |
| 6 | 5 | adantl 481 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 = 𝐶) → {𝐴, 𝐷} = {𝐶, 𝐷}) |
| 7 | 4, 6 | eleqtrd 2843 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) ∧ 𝐴 = 𝐶) → 𝐴 ∈ {𝐶, 𝐷}) |
| 8 | 7 | ex 412 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐶 → 𝐴 ∈ {𝐶, 𝐷})) |
| 9 | | prid2g 4761 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐶, 𝐵}) |
| 10 | 9 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ {𝐶, 𝐵}) |
| 11 | | preq2 4734 |
. . . . . . 7
⊢ (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷}) |
| 12 | 11 | eleq2d 2827 |
. . . . . 6
⊢ (𝐵 = 𝐷 → (𝐵 ∈ {𝐶, 𝐵} ↔ 𝐵 ∈ {𝐶, 𝐷})) |
| 13 | 10, 12 | syl5ibcom 245 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (𝐵 = 𝐷 → 𝐵 ∈ {𝐶, 𝐷})) |
| 14 | 8, 13 | anim12d 609 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}))) |
| 15 | | prid2g 4761 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐶, 𝐴}) |
| 16 | 15 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → 𝐴 ∈ {𝐶, 𝐴}) |
| 17 | | preq2 4734 |
. . . . . . 7
⊢ (𝐴 = 𝐷 → {𝐶, 𝐴} = {𝐶, 𝐷}) |
| 18 | 17 | eleq2d 2827 |
. . . . . 6
⊢ (𝐴 = 𝐷 → (𝐴 ∈ {𝐶, 𝐴} ↔ 𝐴 ∈ {𝐶, 𝐷})) |
| 19 | 16, 18 | syl5ibcom 245 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (𝐴 = 𝐷 → 𝐴 ∈ {𝐶, 𝐷})) |
| 20 | | prid1g 4760 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ {𝐵, 𝐷}) |
| 21 | 20 | 3ad2ant2 1135 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → 𝐵 ∈ {𝐵, 𝐷}) |
| 22 | | preq1 4733 |
. . . . . . 7
⊢ (𝐵 = 𝐶 → {𝐵, 𝐷} = {𝐶, 𝐷}) |
| 23 | 22 | eleq2d 2827 |
. . . . . 6
⊢ (𝐵 = 𝐶 → (𝐵 ∈ {𝐵, 𝐷} ↔ 𝐵 ∈ {𝐶, 𝐷})) |
| 24 | 21, 23 | syl5ibcom 245 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (𝐵 = 𝐶 → 𝐵 ∈ {𝐶, 𝐷})) |
| 25 | 19, 24 | anim12d 609 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}))) |
| 26 | 14, 25 | jaod 860 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)) → (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}))) |
| 27 | | elprg 4648 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) |
| 28 | 27 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (𝐴 ∈ {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷))) |
| 29 | | elprg 4648 |
. . . . . 6
⊢ (𝐵 ∈ 𝑊 → (𝐵 ∈ {𝐶, 𝐷} ↔ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))) |
| 30 | 29 | 3ad2ant2 1135 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (𝐵 ∈ {𝐶, 𝐷} ↔ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))) |
| 31 | 28, 30 | anbi12d 632 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ((𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}) ↔ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))) |
| 32 | | eqtr3 2763 |
. . . . . . . 8
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵) |
| 33 | | eqneqall 2951 |
. . . . . . . 8
⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐵 → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) |
| 34 | 32, 33 | syl 17 |
. . . . . . 7
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → (𝐴 ≠ 𝐵 → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) |
| 35 | | olc 869 |
. . . . . . . 8
⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))) |
| 36 | 35 | a1d 25 |
. . . . . . 7
⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐶) → (𝐴 ≠ 𝐵 → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) |
| 37 | | orc 868 |
. . . . . . . 8
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶))) |
| 38 | 37 | a1d 25 |
. . . . . . 7
⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → (𝐴 ≠ 𝐵 → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) |
| 39 | | eqtr3 2763 |
. . . . . . . 8
⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐷) → 𝐴 = 𝐵) |
| 40 | 39, 33 | syl 17 |
. . . . . . 7
⊢ ((𝐴 = 𝐷 ∧ 𝐵 = 𝐷) → (𝐴 ≠ 𝐵 → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) |
| 41 | 34, 36, 38, 40 | ccase 1038 |
. . . . . 6
⊢ (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) → (𝐴 ≠ 𝐵 → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) |
| 42 | 41 | com12 32 |
. . . . 5
⊢ (𝐴 ≠ 𝐵 → (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) |
| 43 | 42 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) |
| 44 | 31, 43 | sylbid 240 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ((𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}) → ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) |
| 45 | 26, 44 | impbid 212 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → (((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)) ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}))) |
| 46 | 1, 45 | bitrd 279 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 ∈ {𝐶, 𝐷} ∧ 𝐵 ∈ {𝐶, 𝐷}))) |