Metamath Proof Explorer

Theorem eupth2lem2

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

Ref Expression
Hypothesis eupth2lem2.1 ⊢ B ∈ V
Assertion eupth2lem2 ⊢ B ≠ C ∧ B = U → ¬ U ∈ if A = B ∅ A B ↔ U ∈ if A = C ∅ A C

Proof

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