Proof of Theorem eupth2lem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eleq2 2830 | . . 3
⊢ (∅
= if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) → (𝑈 ∈ ∅ ↔ 𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}))) | 
| 2 | 1 | bibi1d 343 | . 2
⊢ (∅
= if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) → ((𝑈 ∈ ∅ ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵))) ↔ (𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵))))) | 
| 3 |  | eleq2 2830 | . . 3
⊢ ({𝐴, 𝐵} = if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) → (𝑈 ∈ {𝐴, 𝐵} ↔ 𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}))) | 
| 4 | 3 | bibi1d 343 | . 2
⊢ ({𝐴, 𝐵} = if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) → ((𝑈 ∈ {𝐴, 𝐵} ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵))) ↔ (𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵))))) | 
| 5 |  | noel 4338 | . . . 4
⊢  ¬
𝑈 ∈
∅ | 
| 6 | 5 | a1i 11 | . . 3
⊢ ((𝑈 ∈ 𝑉 ∧ 𝐴 = 𝐵) → ¬ 𝑈 ∈ ∅) | 
| 7 |  | simpl 482 | . . . . 5
⊢ ((𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵)) → 𝐴 ≠ 𝐵) | 
| 8 | 7 | neneqd 2945 | . . . 4
⊢ ((𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵)) → ¬ 𝐴 = 𝐵) | 
| 9 |  | simpr 484 | . . . 4
⊢ ((𝑈 ∈ 𝑉 ∧ 𝐴 = 𝐵) → 𝐴 = 𝐵) | 
| 10 | 8, 9 | nsyl3 138 | . . 3
⊢ ((𝑈 ∈ 𝑉 ∧ 𝐴 = 𝐵) → ¬ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵))) | 
| 11 | 6, 10 | 2falsed 376 | . 2
⊢ ((𝑈 ∈ 𝑉 ∧ 𝐴 = 𝐵) → (𝑈 ∈ ∅ ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵)))) | 
| 12 |  | elprg 4648 | . . 3
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ {𝐴, 𝐵} ↔ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵))) | 
| 13 |  | df-ne 2941 | . . . 4
⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | 
| 14 |  | ibar 528 | . . . 4
⊢ (𝐴 ≠ 𝐵 → ((𝑈 = 𝐴 ∨ 𝑈 = 𝐵) ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵)))) | 
| 15 | 13, 14 | sylbir 235 | . . 3
⊢ (¬
𝐴 = 𝐵 → ((𝑈 = 𝐴 ∨ 𝑈 = 𝐵) ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵)))) | 
| 16 | 12, 15 | sylan9bb 509 | . 2
⊢ ((𝑈 ∈ 𝑉 ∧ ¬ 𝐴 = 𝐵) → (𝑈 ∈ {𝐴, 𝐵} ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵)))) | 
| 17 | 2, 4, 11, 16 | ifbothda 4564 | 1
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵)))) |