Proof of Theorem prneimg
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | preq12bg 4853 | . . . . 5
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)))) | 
| 2 |  | orddi 1012 | . . . . . 6
⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)) ↔ (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐴 = 𝐶 ∨ 𝐵 = 𝐶)) ∧ ((𝐵 = 𝐷 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐷 ∨ 𝐵 = 𝐶)))) | 
| 3 |  | simpll 767 | . . . . . . 7
⊢ ((((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐴 = 𝐶 ∨ 𝐵 = 𝐶)) ∧ ((𝐵 = 𝐷 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐷 ∨ 𝐵 = 𝐶))) → (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) | 
| 4 |  | pm1.4 870 | . . . . . . . 8
⊢ ((𝐵 = 𝐷 ∨ 𝐵 = 𝐶) → (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) | 
| 5 | 4 | ad2antll 729 | . . . . . . 7
⊢ ((((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐴 = 𝐶 ∨ 𝐵 = 𝐶)) ∧ ((𝐵 = 𝐷 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐷 ∨ 𝐵 = 𝐶))) → (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) | 
| 6 | 3, 5 | jca 511 | . . . . . 6
⊢ ((((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐴 = 𝐶 ∨ 𝐵 = 𝐶)) ∧ ((𝐵 = 𝐷 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐷 ∨ 𝐵 = 𝐶))) → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))) | 
| 7 | 2, 6 | sylbi 217 | . . . . 5
⊢ (((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) ∨ (𝐴 = 𝐷 ∧ 𝐵 = 𝐶)) → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷))) | 
| 8 | 1, 7 | biimtrdi 253 | . . . 4
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} → ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)))) | 
| 9 |  | ianor 984 | . . . . . 6
⊢ (¬
(𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ↔ (¬ 𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷)) | 
| 10 |  | nne 2944 | . . . . . . 7
⊢ (¬
𝐴 ≠ 𝐶 ↔ 𝐴 = 𝐶) | 
| 11 |  | nne 2944 | . . . . . . 7
⊢ (¬
𝐴 ≠ 𝐷 ↔ 𝐴 = 𝐷) | 
| 12 | 10, 11 | orbi12i 915 | . . . . . 6
⊢ ((¬
𝐴 ≠ 𝐶 ∨ ¬ 𝐴 ≠ 𝐷) ↔ (𝐴 = 𝐶 ∨ 𝐴 = 𝐷)) | 
| 13 | 9, 12 | bitr2i 276 | . . . . 5
⊢ ((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ↔ ¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷)) | 
| 14 |  | ianor 984 | . . . . . 6
⊢ (¬
(𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ↔ (¬ 𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷)) | 
| 15 |  | nne 2944 | . . . . . . 7
⊢ (¬
𝐵 ≠ 𝐶 ↔ 𝐵 = 𝐶) | 
| 16 |  | nne 2944 | . . . . . . 7
⊢ (¬
𝐵 ≠ 𝐷 ↔ 𝐵 = 𝐷) | 
| 17 | 15, 16 | orbi12i 915 | . . . . . 6
⊢ ((¬
𝐵 ≠ 𝐶 ∨ ¬ 𝐵 ≠ 𝐷) ↔ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) | 
| 18 | 14, 17 | bitr2i 276 | . . . . 5
⊢ ((𝐵 = 𝐶 ∨ 𝐵 = 𝐷) ↔ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) | 
| 19 | 13, 18 | anbi12i 628 | . . . 4
⊢ (((𝐴 = 𝐶 ∨ 𝐴 = 𝐷) ∧ (𝐵 = 𝐶 ∨ 𝐵 = 𝐷)) ↔ (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷))) | 
| 20 | 8, 19 | imbitrdi 251 | . . 3
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} → (¬ (𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)))) | 
| 21 |  | pm4.56 991 | . . 3
⊢ ((¬
(𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ ¬ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) ↔ ¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷))) | 
| 22 | 20, 21 | imbitrdi 251 | . 2
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ({𝐴, 𝐵} = {𝐶, 𝐷} → ¬ ((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)))) | 
| 23 | 22 | necon2ad 2955 | 1
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∨ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷)) → {𝐴, 𝐵} ≠ {𝐶, 𝐷})) |