Metamath Proof Explorer

Theorem dfon2lem3

Description: Lemma for dfon2 . All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011)

Ref Expression
Assertion dfon2lem3 
|- ( A e. V -> ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( Tr A /\ A. z e. A -. z e. z ) ) )

Proof

Step Hyp Ref Expression
1 untelirr 
 |-  ( A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z -> -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } )
2 eluni2 
 |-  ( z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } <-> E. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } z e. x )
3 vex 
 |-  x e. _V
4 sseq1 
 |-  ( w = x -> ( w C_ A <-> x C_ A ) )
5 treq 
 |-  ( w = x -> ( Tr w <-> Tr x ) )
6 raleq 
 |-  ( w = x -> ( A. t e. w -. t e. t <-> A. t e. x -. t e. t ) )
7 4 5 6 3anbi123d 
 |-  ( w = x -> ( ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) <-> ( x C_ A /\ Tr x /\ A. t e. x -. t e. t ) ) )
8 3 7 elab 
 |-  ( x e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } <-> ( x C_ A /\ Tr x /\ A. t e. x -. t e. t ) )
9 elequ1 
 |-  ( t = z -> ( t e. t <-> z e. t ) )
10 elequ2 
 |-  ( t = z -> ( z e. t <-> z e. z ) )
11 9 10 bitrd 
 |-  ( t = z -> ( t e. t <-> z e. z ) )
12 11 notbid 
 |-  ( t = z -> ( -. t e. t <-> -. z e. z ) )
13 12 cbvralvw 
 |-  ( A. t e. x -. t e. t <-> A. z e. x -. z e. z )
14 13 biimpi 
 |-  ( A. t e. x -. t e. t -> A. z e. x -. z e. z )
15 14 3ad2ant3 
 |-  ( ( x C_ A /\ Tr x /\ A. t e. x -. t e. t ) -> A. z e. x -. z e. z )
16 8 15 sylbi 
 |-  ( x e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> A. z e. x -. z e. z )
17 rsp 
 |-  ( A. z e. x -. z e. z -> ( z e. x -> -. z e. z ) )
18 16 17 syl 
 |-  ( x e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( z e. x -> -. z e. z ) )
19 18 rexlimiv 
 |-  ( E. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } z e. x -> -. z e. z )
20 2 19 sylbi 
 |-  ( z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> -. z e. z )
21 1 20 mprg 
 |-  -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
22 dfon2lem2 
 |-  U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A
23 dfpss2 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A ) )
24 dfon2lem1 
 |-  Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
25 ssexg 
 |-  ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ A e. V ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V )
26 22 25 mpan 
 |-  ( A e. V -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V )
27 psseq1 
 |-  ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( x C. A <-> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A ) )
28 treq 
 |-  ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( Tr x <-> Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
29 27 28 anbi12d 
 |-  ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( ( x C. A /\ Tr x ) <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) ) )
30 eleq1 
 |-  ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( x e. A <-> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A ) )
31 29 30 imbi12d 
 |-  ( x = U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( ( ( x C. A /\ Tr x ) -> x e. A ) <-> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A ) ) )
32 31 spcgv 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V -> ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A ) ) )
33 32 imp 
 |-  ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A ) )
34 26 33 sylan 
 |-  ( ( A e. V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A ) )
35 snssi 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> { U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } } C_ A )
36 unss 
 |-  ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ { U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } } C_ A ) <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } u. { U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } } ) C_ A )
37 df-suc 
 |-  suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } u. { U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } } )
38 37 sseq1i 
 |-  ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A <-> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } u. { U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } } ) C_ A )
39 36 38 sylbb2 
 |-  ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ { U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } } C_ A ) -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A )
40 22 35 39 sylancr 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A )
41 suctr 
 |-  ( Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } )
42 24 41 ax-mp 
 |-  Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
43 untuni 
 |-  ( A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z <-> A. x e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } A. z e. x -. z e. z )
44 43 16 mprgbir 
 |-  A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z
45 nfv 
 |-  F/ t w C_ A
46 nfv 
 |-  F/ t Tr w
47 nfra1 
 |-  F/ t A. t e. w -. t e. t
48 45 46 47 nf3an 
 |-  F/ t ( w C_ A /\ Tr w /\ A. t e. w -. t e. t )
49 48 nfab 
 |-  F/_ t { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
50 49 nfuni 
 |-  F/_ t U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
51 50 untsucf 
 |-  ( A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z -> A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t )
52 44 51 ax-mp 
 |-  A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t
53 sseq1 
 |-  ( z = suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( z C_ A <-> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A ) )
54 treq 
 |-  ( z = suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( Tr z <-> Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
55 nfcv 
 |-  F/_ t z
56 50 nfsuc 
 |-  F/_ t suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) }
57 55 56 raleqf 
 |-  ( z = suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( A. t e. z -. t e. t <-> A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t ) )
58 53 54 57 3anbi123d 
 |-  ( z = suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> ( ( z C_ A /\ Tr z /\ A. t e. z -. t e. t ) <-> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } /\ A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t ) ) )
59 sseq1 
 |-  ( w = z -> ( w C_ A <-> z C_ A ) )
60 treq 
 |-  ( w = z -> ( Tr w <-> Tr z ) )
61 raleq 
 |-  ( w = z -> ( A. t e. w -. t e. t <-> A. t e. z -. t e. t ) )
62 59 60 61 3anbi123d 
 |-  ( w = z -> ( ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) <-> ( z C_ A /\ Tr z /\ A. t e. z -. t e. t ) ) )
63 62 cbvabv 
 |-  { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = { z | ( z C_ A /\ Tr z /\ A. t e. z -. t e. t ) }
64 58 63 elab2g 
 |-  ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V -> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } <-> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } /\ A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t ) ) )
65 64 biimprd 
 |-  ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V -> ( ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } /\ A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t ) -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
66 sucexg 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. _V )
67 65 66 syl11 
 |-  ( ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ Tr suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } /\ A. t e. suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. t e. t ) -> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
68 42 52 67 mp3an23 
 |-  ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A -> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
69 68 com12 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
70 elssuni 
 |-  ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } )
71 sucssel 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
72 70 71 syl5 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
73 69 72 syld 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> ( suc U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
74 40 73 mpd 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. A -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } )
75 34 74 syl6 
 |-  ( ( A e. V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A /\ Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
76 24 75 mpan2i 
 |-  ( ( A e. V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C. A -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
77 23 76 biimtrrid 
 |-  ( ( A e. V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> ( ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } C_ A /\ -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
78 22 77 mpani 
 |-  ( ( A e. V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> ( -. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } ) )
79 21 78 mt3i 
 |-  ( ( A e. V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A )
80 24 44 pm3.2i 
 |-  ( Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } /\ A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z )
81 treq 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A -> ( Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } <-> Tr A ) )
82 raleq 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A -> ( A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z <-> A. z e. A -. z e. z ) )
83 81 82 anbi12d 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A -> ( ( Tr U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } /\ A. z e. U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } -. z e. z ) <-> ( Tr A /\ A. z e. A -. z e. z ) ) )
84 80 83 mpbii 
 |-  ( U. { w | ( w C_ A /\ Tr w /\ A. t e. w -. t e. t ) } = A -> ( Tr A /\ A. z e. A -. z e. z ) )
85 79 84 syl 
 |-  ( ( A e. V /\ A. x ( ( x C. A /\ Tr x ) -> x e. A ) ) -> ( Tr A /\ A. z e. A -. z e. z ) )
86 85 ex 
 |-  ( A e. V -> ( A. x ( ( x C. A /\ Tr x ) -> x e. A ) -> ( Tr A /\ A. z e. A -. z e. z ) ) )