This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eupth2lem2

Description: Lemma for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015)

Ref Expression
Hypothesis eupth2lem2.1 ⊢ 𝐵 ∈ V
Assertion eupth2lem2 ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( ¬ 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ 𝑈 ∈ if ( 𝐴 = 𝐶 , ∅ , { 𝐴 , 𝐶 } ) ) )

Proof

Step Hyp Ref Expression
1 eupth2lem2.1 ⊢ 𝐵 ∈ V
2 eqidd ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → 𝐵 = 𝐵 )
3 2 olcd ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) )
4 3 biantrud ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐴 ≠ 𝐵 ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) ) )
5 eupth2lem1 ⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) ) )
6 1 5 ax-mp ⊢ ( 𝐵 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ ( 𝐴 ≠ 𝐵 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐵 ) ) )
7 4 6 bitr4di ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐴 ≠ 𝐵 ↔ 𝐵 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ) )
8 simpr ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → 𝐵 = 𝑈 )
9 8 eleq1d ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐵 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ) )
10 7 9 bitrd ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐴 ≠ 𝐵 ↔ 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ) )
11 10 necon1bbid ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( ¬ 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ 𝐴 = 𝐵 ) )
12 simpl ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → 𝐵 ≠ 𝐶 )
13 neeq1 ⊢ ( 𝐵 = 𝐴 → ( 𝐵 ≠ 𝐶 ↔ 𝐴 ≠ 𝐶 ) )
14 12 13 syl5ibcom ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐵 = 𝐴 → 𝐴 ≠ 𝐶 ) )
15 14 pm4.71rd ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐵 = 𝐴 ↔ ( 𝐴 ≠ 𝐶 ∧ 𝐵 = 𝐴 ) ) )
16 eqcom ⊢ ( 𝐴 = 𝐵 ↔ 𝐵 = 𝐴 )
17 ancom ⊢ ( ( 𝐵 = 𝐴 ∧ 𝐴 ≠ 𝐶 ) ↔ ( 𝐴 ≠ 𝐶 ∧ 𝐵 = 𝐴 ) )
18 15 16 17 3bitr4g ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐴 = 𝐵 ↔ ( 𝐵 = 𝐴 ∧ 𝐴 ≠ 𝐶 ) ) )
19 12 neneqd ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ¬ 𝐵 = 𝐶 )
20 biorf ⊢ ( ¬ 𝐵 = 𝐶 → ( 𝐵 = 𝐴 ↔ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐴 ) ) )
21 19 20 syl ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐵 = 𝐴 ↔ ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐴 ) ) )
22 orcom ⊢ ( ( 𝐵 = 𝐶 ∨ 𝐵 = 𝐴 ) ↔ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) )
23 21 22 bitrdi ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐵 = 𝐴 ↔ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) )
24 23 anbi1d ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( ( 𝐵 = 𝐴 ∧ 𝐴 ≠ 𝐶 ) ↔ ( ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) ) )
25 18 24 bitrd ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐴 = 𝐵 ↔ ( ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) ) )
26 ancom ⊢ ( ( 𝐴 ≠ 𝐶 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) ↔ ( ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ∧ 𝐴 ≠ 𝐶 ) )
27 25 26 bitr4di ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐴 = 𝐵 ↔ ( 𝐴 ≠ 𝐶 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) ) )
28 eupth2lem1 ⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ if ( 𝐴 = 𝐶 , ∅ , { 𝐴 , 𝐶 } ) ↔ ( 𝐴 ≠ 𝐶 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) ) )
29 1 28 ax-mp ⊢ ( 𝐵 ∈ if ( 𝐴 = 𝐶 , ∅ , { 𝐴 , 𝐶 } ) ↔ ( 𝐴 ≠ 𝐶 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) )
30 8 eleq1d ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( 𝐵 ∈ if ( 𝐴 = 𝐶 , ∅ , { 𝐴 , 𝐶 } ) ↔ 𝑈 ∈ if ( 𝐴 = 𝐶 , ∅ , { 𝐴 , 𝐶 } ) ) )
31 29 30 bitr3id ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( ( 𝐴 ≠ 𝐶 ∧ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) ↔ 𝑈 ∈ if ( 𝐴 = 𝐶 , ∅ , { 𝐴 , 𝐶 } ) ) )
32 11 27 31 3bitrd ⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈 ) → ( ¬ 𝑈 ∈ if ( 𝐴 = 𝐵 , ∅ , { 𝐴 , 𝐵 } ) ↔ 𝑈 ∈ if ( 𝐴 = 𝐶 , ∅ , { 𝐴 , 𝐶 } ) ) )