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∈ifA=B∅AB↔U∈ifA=C∅AC

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∈ifA=B∅AB↔A≠B∧B=A∨B=B
6 1 5 ax-mp ⊢B∈ifA=B∅AB↔A≠B∧B=A∨B=B
7 4 6 bitr4di ⊢B≠C∧B=U→A≠B↔B∈ifA=B∅AB
8 simpr ⊢B≠C∧B=U→B=U
9 8 eleq1d ⊢B≠C∧B=U→B∈ifA=B∅AB↔U∈ifA=B∅AB
10 7 9 bitrd ⊢B≠C∧B=U→A≠B↔U∈ifA=B∅AB
11 10 necon1bbid ⊢B≠C∧B=U→¬U∈ifA=B∅AB↔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∈ifA=C∅AC↔A≠C∧B=A∨B=C
29 1 28 ax-mp ⊢B∈ifA=C∅AC↔A≠C∧B=A∨B=C
30 8 eleq1d ⊢B≠C∧B=U→B∈ifA=C∅AC↔U∈ifA=C∅AC
31 29 30 bitr3id ⊢B≠C∧B=U→A≠C∧B=A∨B=C↔U∈ifA=C∅AC
32 11 27 31 3bitrd ⊢B≠C∧B=U→¬U∈ifA=B∅AB↔U∈ifA=C∅AC