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 } ) ) )