Metamath Proof Explorer

Theorem dfon2lem5

Description: Lemma for dfon2 . Two sets satisfying the new definition also satisfy trichotomy with respect to e. . (Contributed by Scott Fenton, 25-Feb-2011)

Ref Expression
Hypotheses dfon2lem5.1 
|- A e. _V
dfon2lem5.2 
|- B e. _V
Assertion dfon2lem5 
|- ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( A e. B \/ A = B \/ B e. A ) )

Proof

Step Hyp Ref Expression
1 dfon2lem5.1 
 |-  A e. _V
2 dfon2lem5.2 
 |-  B e. _V
3 1 2 dfon2lem4 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( A C_ B \/ B C_ A ) )
4 dfpss2 
 |-  ( A C. B <-> ( A C_ B /\ -. A = B ) )
5 dfpss2 
 |-  ( B C. A <-> ( B C_ A /\ -. B = A ) )
6 eqcom 
 |-  ( B = A <-> A = B )
7 6 notbii 
 |-  ( -. B = A <-> -. A = B )
8 7 anbi2i 
 |-  ( ( B C_ A /\ -. B = A ) <-> ( B C_ A /\ -. A = B ) )
9 5 8 bitri 
 |-  ( B C. A <-> ( B C_ A /\ -. A = B ) )
10 4 9 orbi12i 
 |-  ( ( A C. B \/ B C. A ) <-> ( ( A C_ B /\ -. A = B ) \/ ( B C_ A /\ -. A = B ) ) )
11 andir 
 |-  ( ( ( A C_ B \/ B C_ A ) /\ -. A = B ) <-> ( ( A C_ B /\ -. A = B ) \/ ( B C_ A /\ -. A = B ) ) )
12 10 11 bitr4i 
 |-  ( ( A C. B \/ B C. A ) <-> ( ( A C_ B \/ B C_ A ) /\ -. A = B ) )
13 orcom 
 |-  ( ( A C. B \/ B C. A ) <-> ( B C. A \/ A C. B ) )
14 dfon2lem3 
 |-  ( B e. _V -> ( A. y ( ( y C. B /\ Tr y ) -> y e. B ) -> ( Tr B /\ A. z e. B -. z e. z ) ) )
15 2 14 ax-mp 
 |-  ( A. y ( ( y C. B /\ Tr y ) -> y e. B ) -> ( Tr B /\ A. z e. B -. z e. z ) )
16 15 simpld 
 |-  ( A. y ( ( y C. B /\ Tr y ) -> y e. B ) -> Tr B )
17 psseq1 
 |-  ( x = B -> ( x C. A <-> B C. A ) )
18 treq 
 |-  ( x = B -> ( Tr x <-> Tr B ) )
19 17 18 anbi12d 
 |-  ( x = B -> ( ( x C. A /\ Tr x ) <-> ( B C. A /\ Tr B ) ) )
20 eleq1 
 |-  ( x = B -> ( x e. A <-> B e. A ) )
21 19 20 imbi12d 
 |-  ( x = B -> ( ( ( x C. A /\ Tr x ) -> x e. A ) <-> ( ( B C. A /\ Tr B ) -> B e. A ) ) )
22 2 21 spcv 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( ( B C. A /\ Tr B ) -> B e. A ) )
23 22 expcomd 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( Tr B -> ( B C. A -> B e. A ) ) )
24 23 imp 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ Tr B ) -> ( B C. A -> B e. A ) )
25 16 24 sylan2 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( B C. A -> B e. A ) )
26 dfon2lem3 
 |-  ( A e. _V -> ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( Tr A /\ A. z e. A -. z e. z ) ) )
27 1 26 ax-mp 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( Tr A /\ A. z e. A -. z e. z ) )
28 27 simpld 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> Tr A )
29 psseq1 
 |-  ( y = A -> ( y C. B <-> A C. B ) )
30 treq 
 |-  ( y = A -> ( Tr y <-> Tr A ) )
31 29 30 anbi12d 
 |-  ( y = A -> ( ( y C. B /\ Tr y ) <-> ( A C. B /\ Tr A ) ) )
32 eleq1 
 |-  ( y = A -> ( y e. B <-> A e. B ) )
33 31 32 imbi12d 
 |-  ( y = A -> ( ( ( y C. B /\ Tr y ) -> y e. B ) <-> ( ( A C. B /\ Tr A ) -> A e. B ) ) )
34 1 33 spcv 
 |-  ( A. y ( ( y C. B /\ Tr y ) -> y e. B ) -> ( ( A C. B /\ Tr A ) -> A e. B ) )
35 34 expcomd 
 |-  ( A. y ( ( y C. B /\ Tr y ) -> y e. B ) -> ( Tr A -> ( A C. B -> A e. B ) ) )
36 28 35 mpan9 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( A C. B -> A e. B ) )
37 25 36 orim12d 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( ( B C. A \/ A C. B ) -> ( B e. A \/ A e. B ) ) )
38 13 37 syl5bi 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( ( A C. B \/ B C. A ) -> ( B e. A \/ A e. B ) ) )
39 12 38 syl5bir 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( ( ( A C_ B \/ B C_ A ) /\ -. A = B ) -> ( B e. A \/ A e. B ) ) )
40 3 39 mpand 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( -. A = B -> ( B e. A \/ A e. B ) ) )
41 3orrot 
 |-  ( ( A e. B \/ A = B \/ B e. A ) <-> ( A = B \/ B e. A \/ A e. B ) )
42 3orass 
 |-  ( ( A = B \/ B e. A \/ A e. B ) <-> ( A = B \/ ( B e. A \/ A e. B ) ) )
43 df-or 
 |-  ( ( A = B \/ ( B e. A \/ A e. B ) ) <-> ( -. A = B -> ( B e. A \/ A e. B ) ) )
44 42 43 bitri 
 |-  ( ( A = B \/ B e. A \/ A e. B ) <-> ( -. A = B -> ( B e. A \/ A e. B ) ) )
45 41 44 bitri 
 |-  ( ( A e. B \/ A = B \/ B e. A ) <-> ( -. A = B -> ( B e. A \/ A e. B ) ) )
46 40 45 sylibr 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( A e. B \/ A = B \/ B e. A ) )