Metamath Proof Explorer

Theorem dfon2lem8

Description: Lemma for dfon2 . The intersection of a nonempty class A of new ordinals is itself a new ordinal and is contained within A (Contributed by Scott Fenton, 26-Feb-2011)

Ref Expression
Assertion dfon2lem8 
|- ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) /\ |^| A e. A ) )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 dfon2lem3 
 |-  ( x e. _V -> ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( Tr x /\ A. z e. x -. z e. z ) ) )
3 1 2 ax-mp 
 |-  ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( Tr x /\ A. z e. x -. z e. z ) )
4 3 simpld 
 |-  ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> Tr x )
5 4 ralimi 
 |-  ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> A. x e. A Tr x )
6 trint 
 |-  ( A. x e. A Tr x -> Tr |^| A )
7 5 6 syl 
 |-  ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> Tr |^| A )
8 7 adantl 
 |-  ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> Tr |^| A )
9 1 dfon2lem7 
 |-  ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
10 9 alrimiv 
 |-  ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
11 10 ralimi 
 |-  ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> A. x e. A A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
12 df-ral 
 |-  ( A. x e. A A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> A. x ( x e. A -> A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) )
13 19.21v 
 |-  ( A. w ( x e. A -> ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) <-> ( x e. A -> A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) )
14 13 albii 
 |-  ( A. x A. w ( x e. A -> ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) <-> A. x ( x e. A -> A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) )
15 12 14 bitr4i 
 |-  ( A. x e. A A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> A. x A. w ( x e. A -> ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) )
16 impexp 
 |-  ( ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> ( x e. A -> ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) )
17 16 2albii 
 |-  ( A. x A. w ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> A. x A. w ( x e. A -> ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) )
18 eluni2 
 |-  ( w e. U. A <-> E. x e. A w e. x )
19 18 biimpi 
 |-  ( w e. U. A -> E. x e. A w e. x )
20 19 imim1i 
 |-  ( ( E. x e. A w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) -> ( w e. U. A -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
21 20 alimi 
 |-  ( A. w ( E. x e. A w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) -> A. w ( w e. U. A -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
22 alcom 
 |-  ( A. x A. w ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> A. w A. x ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
23 19.23v 
 |-  ( A. x ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> ( E. x ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
24 df-rex 
 |-  ( E. x e. A w e. x <-> E. x ( x e. A /\ w e. x ) )
25 24 imbi1i 
 |-  ( ( E. x e. A w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> ( E. x ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
26 23 25 bitr4i 
 |-  ( A. x ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> ( E. x e. A w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
27 26 albii 
 |-  ( A. w A. x ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> A. w ( E. x e. A w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
28 22 27 bitri 
 |-  ( A. x A. w ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) <-> A. w ( E. x e. A w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
29 df-ral 
 |-  ( A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) <-> A. w ( w e. U. A -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
30 21 28 29 3imtr4i 
 |-  ( A. x A. w ( ( x e. A /\ w e. x ) -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) -> A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) )
31 17 30 sylbir 
 |-  ( A. x A. w ( x e. A -> ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) ) -> A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) )
32 15 31 sylbi 
 |-  ( A. x e. A A. w ( w e. x -> A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) -> A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) )
33 11 32 syl 
 |-  ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) )
34 33 adantl 
 |-  ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) )
35 intssuni 
 |-  ( A =/= (/) -> |^| A C_ U. A )
36 ssralv 
 |-  ( |^| A C_ U. A -> ( A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) -> A. w e. |^| A A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
37 35 36 syl 
 |-  ( A =/= (/) -> ( A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) -> A. w e. |^| A A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
38 37 adantr 
 |-  ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( A. w e. U. A A. t ( ( t C. w /\ Tr t ) -> t e. w ) -> A. w e. |^| A A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) )
39 34 38 mpd 
 |-  ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> A. w e. |^| A A. t ( ( t C. w /\ Tr t ) -> t e. w ) )
40 dfon2lem6 
 |-  ( ( Tr |^| A /\ A. w e. |^| A A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) -> A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) )
41 intex 
 |-  ( A =/= (/) <-> |^| A e. _V )
42 dfon2lem3 
 |-  ( |^| A e. _V -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) -> ( Tr |^| A /\ A. t e. |^| A -. t e. t ) ) )
43 41 42 sylbi 
 |-  ( A =/= (/) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) -> ( Tr |^| A /\ A. t e. |^| A -. t e. t ) ) )
44 43 imp 
 |-  ( ( A =/= (/) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( Tr |^| A /\ A. t e. |^| A -. t e. t ) )
45 44 simprd 
 |-  ( ( A =/= (/) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> A. t e. |^| A -. t e. t )
46 untelirr 
 |-  ( A. t e. |^| A -. t e. t -> -. |^| A e. |^| A )
47 45 46 syl 
 |-  ( ( A =/= (/) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> -. |^| A e. |^| A )
48 47 adantlr 
 |-  ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> -. |^| A e. |^| A )
49 risset 
 |-  ( |^| A e. A <-> E. t e. A t = |^| A )
50 49 notbii 
 |-  ( -. |^| A e. A <-> -. E. t e. A t = |^| A )
51 ralnex 
 |-  ( A. t e. A -. t = |^| A <-> -. E. t e. A t = |^| A )
52 50 51 bitr4i 
 |-  ( -. |^| A e. A <-> A. t e. A -. t = |^| A )
53 eqcom 
 |-  ( t = |^| A <-> |^| A = t )
54 53 notbii 
 |-  ( -. t = |^| A <-> -. |^| A = t )
55 44 simpld 
 |-  ( ( A =/= (/) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> Tr |^| A )
56 55 adantlr 
 |-  ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> Tr |^| A )
57 psseq2 
 |-  ( x = t -> ( y C. x <-> y C. t ) )
58 57 anbi1d 
 |-  ( x = t -> ( ( y C. x /\ Tr y ) <-> ( y C. t /\ Tr y ) ) )
59 elequ2 
 |-  ( x = t -> ( y e. x <-> y e. t ) )
60 58 59 imbi12d 
 |-  ( x = t -> ( ( ( y C. x /\ Tr y ) -> y e. x ) <-> ( ( y C. t /\ Tr y ) -> y e. t ) ) )
61 60 albidv 
 |-  ( x = t -> ( A. y ( ( y C. x /\ Tr y ) -> y e. x ) <-> A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) )
62 61 rspccv 
 |-  ( A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) -> ( t e. A -> A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) )
63 62 adantl 
 |-  ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( t e. A -> A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) )
64 intss1 
 |-  ( t e. A -> |^| A C_ t )
65 dfpss2 
 |-  ( |^| A C. t <-> ( |^| A C_ t /\ -. |^| A = t ) )
66 psseq1 
 |-  ( y = |^| A -> ( y C. t <-> |^| A C. t ) )
67 treq 
 |-  ( y = |^| A -> ( Tr y <-> Tr |^| A ) )
68 66 67 anbi12d 
 |-  ( y = |^| A -> ( ( y C. t /\ Tr y ) <-> ( |^| A C. t /\ Tr |^| A ) ) )
69 eleq1 
 |-  ( y = |^| A -> ( y e. t <-> |^| A e. t ) )
70 68 69 imbi12d 
 |-  ( y = |^| A -> ( ( ( y C. t /\ Tr y ) -> y e. t ) <-> ( ( |^| A C. t /\ Tr |^| A ) -> |^| A e. t ) ) )
71 70 spcgv 
 |-  ( |^| A e. _V -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( ( |^| A C. t /\ Tr |^| A ) -> |^| A e. t ) ) )
72 41 71 sylbi 
 |-  ( A =/= (/) -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( ( |^| A C. t /\ Tr |^| A ) -> |^| A e. t ) ) )
73 72 imp 
 |-  ( ( A =/= (/) /\ A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) -> ( ( |^| A C. t /\ Tr |^| A ) -> |^| A e. t ) )
74 73 expd 
 |-  ( ( A =/= (/) /\ A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) -> ( |^| A C. t -> ( Tr |^| A -> |^| A e. t ) ) )
75 65 74 biimtrrid 
 |-  ( ( A =/= (/) /\ A. y ( ( y C. t /\ Tr y ) -> y e. t ) ) -> ( ( |^| A C_ t /\ -. |^| A = t ) -> ( Tr |^| A -> |^| A e. t ) ) )
76 75 exp4b 
 |-  ( A =/= (/) -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( |^| A C_ t -> ( -. |^| A = t -> ( Tr |^| A -> |^| A e. t ) ) ) ) )
77 76 com45 
 |-  ( A =/= (/) -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( |^| A C_ t -> ( Tr |^| A -> ( -. |^| A = t -> |^| A e. t ) ) ) ) )
78 77 com23 
 |-  ( A =/= (/) -> ( |^| A C_ t -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( Tr |^| A -> ( -. |^| A = t -> |^| A e. t ) ) ) ) )
79 64 78 syl5 
 |-  ( A =/= (/) -> ( t e. A -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( Tr |^| A -> ( -. |^| A = t -> |^| A e. t ) ) ) ) )
80 79 adantr 
 |-  ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( t e. A -> ( A. y ( ( y C. t /\ Tr y ) -> y e. t ) -> ( Tr |^| A -> ( -. |^| A = t -> |^| A e. t ) ) ) ) )
81 63 80 mpdd 
 |-  ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( t e. A -> ( Tr |^| A -> ( -. |^| A = t -> |^| A e. t ) ) ) )
82 81 adantr 
 |-  ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( t e. A -> ( Tr |^| A -> ( -. |^| A = t -> |^| A e. t ) ) ) )
83 56 82 mpid 
 |-  ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( t e. A -> ( -. |^| A = t -> |^| A e. t ) ) )
84 54 83 syl7bi 
 |-  ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( t e. A -> ( -. t = |^| A -> |^| A e. t ) ) )
85 84 ralrimiv 
 |-  ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> A. t e. A ( -. t = |^| A -> |^| A e. t ) )
86 ralim 
 |-  ( A. t e. A ( -. t = |^| A -> |^| A e. t ) -> ( A. t e. A -. t = |^| A -> A. t e. A |^| A e. t ) )
87 85 86 syl 
 |-  ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( A. t e. A -. t = |^| A -> A. t e. A |^| A e. t ) )
88 52 87 biimtrid 
 |-  ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( -. |^| A e. A -> A. t e. A |^| A e. t ) )
89 elintg 
 |-  ( |^| A e. _V -> ( |^| A e. |^| A <-> A. t e. A |^| A e. t ) )
90 41 89 sylbi 
 |-  ( A =/= (/) -> ( |^| A e. |^| A <-> A. t e. A |^| A e. t ) )
91 90 ad2antrr 
 |-  ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( |^| A e. |^| A <-> A. t e. A |^| A e. t ) )
92 88 91 sylibrd 
 |-  ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> ( -. |^| A e. A -> |^| A e. |^| A ) )
93 48 92 mt3d 
 |-  ( ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) /\ A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) ) -> |^| A e. A )
94 93 ex 
 |-  ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) -> |^| A e. A ) )
95 94 ancld 
 |-  ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) /\ |^| A e. A ) ) )
96 40 95 syl5 
 |-  ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( ( Tr |^| A /\ A. w e. |^| A A. t ( ( t C. w /\ Tr t ) -> t e. w ) ) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) /\ |^| A e. A ) ) )
97 8 39 96 mp2and 
 |-  ( ( A =/= (/) /\ A. x e. A A. y ( ( y C. x /\ Tr y ) -> y e. x ) ) -> ( A. z ( ( z C. |^| A /\ Tr z ) -> z e. |^| A ) /\ |^| A e. A ) )