Metamath Proof Explorer

Theorem dfon2lem4

Description: Lemma for dfon2 . If two sets satisfy the new definition, then one is a subset of the other. (Contributed by Scott Fenton, 25-Feb-2011)

Ref Expression
Hypotheses dfon2lem4.1 
|- A e. _V
dfon2lem4.2 
|- B e. _V
Assertion 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 ) )

Proof

Step Hyp Ref Expression
1 dfon2lem4.1 
 |-  A e. _V
2 dfon2lem4.2 
 |-  B e. _V
3 inss1 
 |-  ( A i^i B ) C_ A
4 3 sseli 
 |-  ( ( A i^i B ) e. ( A i^i B ) -> ( A i^i B ) e. A )
5 dfon2lem3 
 |-  ( A e. _V -> ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( Tr A /\ A. z e. A -. z e. z ) ) )
6 1 5 ax-mp 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( Tr A /\ A. z e. A -. z e. z ) )
7 6 simprd 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> A. z e. A -. z e. z )
8 eleq1 
 |-  ( z = ( A i^i B ) -> ( z e. z <-> ( A i^i B ) e. z ) )
9 eleq2 
 |-  ( z = ( A i^i B ) -> ( ( A i^i B ) e. z <-> ( A i^i B ) e. ( A i^i B ) ) )
10 8 9 bitrd 
 |-  ( z = ( A i^i B ) -> ( z e. z <-> ( A i^i B ) e. ( A i^i B ) ) )
11 10 notbid 
 |-  ( z = ( A i^i B ) -> ( -. z e. z <-> -. ( A i^i B ) e. ( A i^i B ) ) )
12 11 rspccv 
 |-  ( A. z e. A -. z e. z -> ( ( A i^i B ) e. A -> -. ( A i^i B ) e. ( A i^i B ) ) )
13 7 12 syl 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( ( A i^i B ) e. A -> -. ( A i^i B ) e. ( A i^i B ) ) )
14 13 adantr 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( ( A i^i B ) e. A -> -. ( A i^i B ) e. ( A i^i B ) ) )
15 4 14 syl5 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( ( A i^i B ) e. ( A i^i B ) -> -. ( A i^i B ) e. ( A i^i B ) ) )
16 15 pm2.01d 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> -. ( A i^i B ) e. ( A i^i B ) )
17 elin 
 |-  ( ( A i^i B ) e. ( A i^i B ) <-> ( ( A i^i B ) e. A /\ ( A i^i B ) e. B ) )
18 16 17 sylnib 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> -. ( ( A i^i B ) e. A /\ ( A i^i B ) e. B ) )
19 6 simpld 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> Tr A )
20 dfon2lem3 
 |-  ( B e. _V -> ( A. y ( ( y C. B /\ Tr y ) -> y e. B ) -> ( Tr B /\ A. z e. B -. z e. z ) ) )
21 2 20 ax-mp 
 |-  ( A. y ( ( y C. B /\ Tr y ) -> y e. B ) -> ( Tr B /\ A. z e. B -. z e. z ) )
22 21 simpld 
 |-  ( A. y ( ( y C. B /\ Tr y ) -> y e. B ) -> Tr B )
23 trin 
 |-  ( ( Tr A /\ Tr B ) -> Tr ( A i^i B ) )
24 19 22 23 syl2an 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> Tr ( A i^i B ) )
25 1 inex1 
 |-  ( A i^i B ) e. _V
26 psseq1 
 |-  ( x = ( A i^i B ) -> ( x C. A <-> ( A i^i B ) C. A ) )
27 treq 
 |-  ( x = ( A i^i B ) -> ( Tr x <-> Tr ( A i^i B ) ) )
28 26 27 anbi12d 
 |-  ( x = ( A i^i B ) -> ( ( x C. A /\ Tr x ) <-> ( ( A i^i B ) C. A /\ Tr ( A i^i B ) ) ) )
29 eleq1 
 |-  ( x = ( A i^i B ) -> ( x e. A <-> ( A i^i B ) e. A ) )
30 28 29 imbi12d 
 |-  ( x = ( A i^i B ) -> ( ( ( x C. A /\ Tr x ) -> x e. A ) <-> ( ( ( A i^i B ) C. A /\ Tr ( A i^i B ) ) -> ( A i^i B ) e. A ) ) )
31 25 30 spcv 
 |-  ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( ( ( A i^i B ) C. A /\ Tr ( A i^i B ) ) -> ( A i^i B ) e. A ) )
32 31 adantr 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( ( ( A i^i B ) C. A /\ Tr ( A i^i B ) ) -> ( A i^i B ) e. A ) )
33 24 32 mpan2d 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( ( A i^i B ) C. A -> ( A i^i B ) e. A ) )
34 psseq1 
 |-  ( y = ( A i^i B ) -> ( y C. B <-> ( A i^i B ) C. B ) )
35 treq 
 |-  ( y = ( A i^i B ) -> ( Tr y <-> Tr ( A i^i B ) ) )
36 34 35 anbi12d 
 |-  ( y = ( A i^i B ) -> ( ( y C. B /\ Tr y ) <-> ( ( A i^i B ) C. B /\ Tr ( A i^i B ) ) ) )
37 eleq1 
 |-  ( y = ( A i^i B ) -> ( y e. B <-> ( A i^i B ) e. B ) )
38 36 37 imbi12d 
 |-  ( y = ( A i^i B ) -> ( ( ( y C. B /\ Tr y ) -> y e. B ) <-> ( ( ( A i^i B ) C. B /\ Tr ( A i^i B ) ) -> ( A i^i B ) e. B ) ) )
39 25 38 spcv 
 |-  ( A. y ( ( y C. B /\ Tr y ) -> y e. B ) -> ( ( ( A i^i B ) C. B /\ Tr ( A i^i B ) ) -> ( A i^i B ) e. B ) )
40 39 adantl 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( ( ( A i^i B ) C. B /\ Tr ( A i^i B ) ) -> ( A i^i B ) e. B ) )
41 24 40 mpan2d 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( ( A i^i B ) C. B -> ( A i^i B ) e. B ) )
42 33 41 anim12d 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( ( ( A i^i B ) C. A /\ ( A i^i B ) C. B ) -> ( ( A i^i B ) e. A /\ ( A i^i B ) e. B ) ) )
43 18 42 mtod 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> -. ( ( A i^i B ) C. A /\ ( A i^i B ) C. B ) )
44 ianor 
 |-  ( -. ( ( A i^i B ) C. A /\ ( A i^i B ) C. B ) <-> ( -. ( A i^i B ) C. A \/ -. ( A i^i B ) C. B ) )
45 43 44 sylib 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( -. ( A i^i B ) C. A \/ -. ( A i^i B ) C. B ) )
46 sspss 
 |-  ( ( A i^i B ) C_ A <-> ( ( A i^i B ) C. A \/ ( A i^i B ) = A ) )
47 3 46 mpbi 
 |-  ( ( A i^i B ) C. A \/ ( A i^i B ) = A )
48 inss2 
 |-  ( A i^i B ) C_ B
49 sspss 
 |-  ( ( A i^i B ) C_ B <-> ( ( A i^i B ) C. B \/ ( A i^i B ) = B ) )
50 48 49 mpbi 
 |-  ( ( A i^i B ) C. B \/ ( A i^i B ) = B )
51 orel1 
 |-  ( -. ( A i^i B ) C. A -> ( ( ( A i^i B ) C. A \/ ( A i^i B ) = A ) -> ( A i^i B ) = A ) )
52 orc 
 |-  ( ( A i^i B ) = A -> ( ( A i^i B ) = A \/ ( A i^i B ) = B ) )
53 51 52 syl6 
 |-  ( -. ( A i^i B ) C. A -> ( ( ( A i^i B ) C. A \/ ( A i^i B ) = A ) -> ( ( A i^i B ) = A \/ ( A i^i B ) = B ) ) )
54 orel1 
 |-  ( -. ( A i^i B ) C. B -> ( ( ( A i^i B ) C. B \/ ( A i^i B ) = B ) -> ( A i^i B ) = B ) )
55 olc 
 |-  ( ( A i^i B ) = B -> ( ( A i^i B ) = A \/ ( A i^i B ) = B ) )
56 54 55 syl6 
 |-  ( -. ( A i^i B ) C. B -> ( ( ( A i^i B ) C. B \/ ( A i^i B ) = B ) -> ( ( A i^i B ) = A \/ ( A i^i B ) = B ) ) )
57 53 56 jaoa 
 |-  ( ( -. ( A i^i B ) C. A \/ -. ( A i^i B ) C. B ) -> ( ( ( ( A i^i B ) C. A \/ ( A i^i B ) = A ) /\ ( ( A i^i B ) C. B \/ ( A i^i B ) = B ) ) -> ( ( A i^i B ) = A \/ ( A i^i B ) = B ) ) )
58 47 50 57 mp2ani 
 |-  ( ( -. ( A i^i B ) C. A \/ -. ( A i^i B ) C. B ) -> ( ( A i^i B ) = A \/ ( A i^i B ) = B ) )
59 45 58 syl 
 |-  ( ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) /\ A. y ( ( y C. B /\ Tr y ) -> y e. B ) ) -> ( ( A i^i B ) = A \/ ( A i^i B ) = B ) )
60 df-ss 
 |-  ( A C_ B <-> ( A i^i B ) = A )
61 sseqin2 
 |-  ( B C_ A <-> ( A i^i B ) = B )
62 60 61 orbi12i 
 |-  ( ( A C_ B \/ B C_ A ) <-> ( ( A i^i B ) = A \/ ( A i^i B ) = B ) )
63 59 62 sylibr 
 |-  ( ( 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 ) )