Metamath Proof Explorer

Theorem eupth2lem2

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

Ref Expression
Hypothesis eupth2lem2.1 
|- B e. _V
Assertion eupth2lem2 
|- ( ( B =/= C /\ B = U ) -> ( -. U e. if ( A = B , (/) , { A , B } ) <-> U e. if ( A = C , (/) , { A , C } ) ) )

Proof

Step Hyp Ref Expression
1 eupth2lem2.1 
 |-  B e. _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 e. _V -> ( B e. if ( A = B , (/) , { A , B } ) <-> ( A =/= B /\ ( B = A \/ B = B ) ) ) )
6 1 5 ax-mp 
 |-  ( B e. if ( A = B , (/) , { A , B } ) <-> ( A =/= B /\ ( B = A \/ B = B ) ) )
7 4 6 bitr4di 
 |-  ( ( B =/= C /\ B = U ) -> ( A =/= B <-> B e. if ( A = B , (/) , { A , B } ) ) )
8 simpr 
 |-  ( ( B =/= C /\ B = U ) -> B = U )
9 8 eleq1d 
 |-  ( ( B =/= C /\ B = U ) -> ( B e. if ( A = B , (/) , { A , B } ) <-> U e. if ( A = B , (/) , { A , B } ) ) )
10 7 9 bitrd 
 |-  ( ( B =/= C /\ B = U ) -> ( A =/= B <-> U e. if ( A = B , (/) , { A , B } ) ) )
11 10 necon1bbid 
 |-  ( ( B =/= C /\ B = U ) -> ( -. U e. 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 e. _V -> ( B e. if ( A = C , (/) , { A , C } ) <-> ( A =/= C /\ ( B = A \/ B = C ) ) ) )
29 1 28 ax-mp 
 |-  ( B e. if ( A = C , (/) , { A , C } ) <-> ( A =/= C /\ ( B = A \/ B = C ) ) )
30 8 eleq1d 
 |-  ( ( B =/= C /\ B = U ) -> ( B e. if ( A = C , (/) , { A , C } ) <-> U e. if ( A = C , (/) , { A , C } ) ) )
31 29 30 bitr3id 
 |-  ( ( B =/= C /\ B = U ) -> ( ( A =/= C /\ ( B = A \/ B = C ) ) <-> U e. if ( A = C , (/) , { A , C } ) ) )
32 11 27 31 3bitrd 
 |-  ( ( B =/= C /\ B = U ) -> ( -. U e. if ( A = B , (/) , { A , B } ) <-> U e. if ( A = C , (/) , { A , C } ) ) )