Metamath Proof Explorer

Theorem tskuni

Description: The union of an element of a transitive Tarski class is in the set. (Contributed by Mario Carneiro, 22-Jun-2013)

Ref Expression
Assertion tskuni 
|- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> U. A e. T )

Proof

Step Hyp Ref Expression
1 tsksdom 
 |-  ( ( T e. Tarski /\ A e. T ) -> A ~< T )
2 cardidg 
 |-  ( T e. Tarski -> ( card ` T ) ~~ T )
3 2 ensymd 
 |-  ( T e. Tarski -> T ~~ ( card ` T ) )
4 3 adantr 
 |-  ( ( T e. Tarski /\ A e. T ) -> T ~~ ( card ` T ) )
5 sdomentr 
 |-  ( ( A ~< T /\ T ~~ ( card ` T ) ) -> A ~< ( card ` T ) )
6 1 4 5 syl2anc 
 |-  ( ( T e. Tarski /\ A e. T ) -> A ~< ( card ` T ) )
7 eqid 
 |-  ( x e. A |-> ( f " x ) ) = ( x e. A |-> ( f " x ) )
8 7 rnmpt 
 |-  ran ( x e. A |-> ( f " x ) ) = { z | E. x e. A z = ( f " x ) }
9 cardon 
 |-  ( card ` T ) e. On
10 sdomdom 
 |-  ( A ~< ( card ` T ) -> A ~<_ ( card ` T ) )
11 ondomen 
 |-  ( ( ( card ` T ) e. On /\ A ~<_ ( card ` T ) ) -> A e. dom card )
12 9 10 11 sylancr 
 |-  ( A ~< ( card ` T ) -> A e. dom card )
13 12 adantl 
 |-  ( ( A e. T /\ A ~< ( card ` T ) ) -> A e. dom card )
14 vex 
 |-  f e. _V
15 14 imaex 
 |-  ( f " x ) e. _V
16 15 7 fnmpti 
 |-  ( x e. A |-> ( f " x ) ) Fn A
17 dffn4 
 |-  ( ( x e. A |-> ( f " x ) ) Fn A <-> ( x e. A |-> ( f " x ) ) : A -onto-> ran ( x e. A |-> ( f " x ) ) )
18 16 17 mpbi 
 |-  ( x e. A |-> ( f " x ) ) : A -onto-> ran ( x e. A |-> ( f " x ) )
19 fodomnum 
 |-  ( A e. dom card -> ( ( x e. A |-> ( f " x ) ) : A -onto-> ran ( x e. A |-> ( f " x ) ) -> ran ( x e. A |-> ( f " x ) ) ~<_ A ) )
20 13 18 19 mpisyl 
 |-  ( ( A e. T /\ A ~< ( card ` T ) ) -> ran ( x e. A |-> ( f " x ) ) ~<_ A )
21 8 20 eqbrtrrid 
 |-  ( ( A e. T /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~<_ A )
22 domsdomtr 
 |-  ( ( { z | E. x e. A z = ( f " x ) } ~<_ A /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
23 21 22 sylancom 
 |-  ( ( A e. T /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
24 23 adantll 
 |-  ( ( ( T e. Tarski /\ A e. T ) /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
25 6 24 mpdan 
 |-  ( ( T e. Tarski /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
26 ne0i 
 |-  ( A e. T -> T =/= (/) )
27 tskcard 
 |-  ( ( T e. Tarski /\ T =/= (/) ) -> ( card ` T ) e. Inacc )
28 26 27 sylan2 
 |-  ( ( T e. Tarski /\ A e. T ) -> ( card ` T ) e. Inacc )
29 elina 
 |-  ( ( card ` T ) e. Inacc <-> ( ( card ` T ) =/= (/) /\ ( cf ` ( card ` T ) ) = ( card ` T ) /\ A. x e. ( card ` T ) ~P x ~< ( card ` T ) ) )
30 29 simp2bi 
 |-  ( ( card ` T ) e. Inacc -> ( cf ` ( card ` T ) ) = ( card ` T ) )
31 28 30 syl 
 |-  ( ( T e. Tarski /\ A e. T ) -> ( cf ` ( card ` T ) ) = ( card ` T ) )
32 25 31 breqtrrd 
 |-  ( ( T e. Tarski /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) )
33 32 3adant2 
 |-  ( ( T e. Tarski /\ Tr T /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) )
34 33 adantr 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) )
35 28 3adant2 
 |-  ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( card ` T ) e. Inacc )
36 35 adantr 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> ( card ` T ) e. Inacc )
37 inawina 
 |-  ( ( card ` T ) e. Inacc -> ( card ` T ) e. InaccW )
38 winalim 
 |-  ( ( card ` T ) e. InaccW -> Lim ( card ` T ) )
39 36 37 38 3syl 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> Lim ( card ` T ) )
40 vex 
 |-  y e. _V
41 eqeq1 
 |-  ( z = y -> ( z = ( f " x ) <-> y = ( f " x ) ) )
42 41 rexbidv 
 |-  ( z = y -> ( E. x e. A z = ( f " x ) <-> E. x e. A y = ( f " x ) ) )
43 40 42 elab 
 |-  ( y e. { z | E. x e. A z = ( f " x ) } <-> E. x e. A y = ( f " x ) )
44 imassrn 
 |-  ( f " x ) C_ ran f
45 f1ofo 
 |-  ( f : U. A -1-1-onto-> ( card ` T ) -> f : U. A -onto-> ( card ` T ) )
46 forn 
 |-  ( f : U. A -onto-> ( card ` T ) -> ran f = ( card ` T ) )
47 45 46 syl 
 |-  ( f : U. A -1-1-onto-> ( card ` T ) -> ran f = ( card ` T ) )
48 44 47 sseqtrid 
 |-  ( f : U. A -1-1-onto-> ( card ` T ) -> ( f " x ) C_ ( card ` T ) )
49 48 ad2antlr 
 |-  ( ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) /\ x e. A ) -> ( f " x ) C_ ( card ` T ) )
50 f1of1 
 |-  ( f : U. A -1-1-onto-> ( card ` T ) -> f : U. A -1-1-> ( card ` T ) )
51 elssuni 
 |-  ( x e. A -> x C_ U. A )
52 vex 
 |-  x e. _V
53 52 f1imaen 
 |-  ( ( f : U. A -1-1-> ( card ` T ) /\ x C_ U. A ) -> ( f " x ) ~~ x )
54 50 51 53 syl2an 
 |-  ( ( f : U. A -1-1-onto-> ( card ` T ) /\ x e. A ) -> ( f " x ) ~~ x )
55 54 adantll 
 |-  ( ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) /\ x e. A ) -> ( f " x ) ~~ x )
56 simpl1 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> T e. Tarski )
57 trss 
 |-  ( Tr T -> ( A e. T -> A C_ T ) )
58 57 imp 
 |-  ( ( Tr T /\ A e. T ) -> A C_ T )
59 58 3adant1 
 |-  ( ( T e. Tarski /\ Tr T /\ A e. T ) -> A C_ T )
60 59 sselda 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x e. T )
61 tsksdom 
 |-  ( ( T e. Tarski /\ x e. T ) -> x ~< T )
62 56 60 61 syl2anc 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x ~< T )
63 56 3 syl 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> T ~~ ( card ` T ) )
64 sdomentr 
 |-  ( ( x ~< T /\ T ~~ ( card ` T ) ) -> x ~< ( card ` T ) )
65 62 63 64 syl2anc 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x ~< ( card ` T ) )
66 65 adantlr 
 |-  ( ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) /\ x e. A ) -> x ~< ( card ` T ) )
67 ensdomtr 
 |-  ( ( ( f " x ) ~~ x /\ x ~< ( card ` T ) ) -> ( f " x ) ~< ( card ` T ) )
68 55 66 67 syl2anc 
 |-  ( ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) /\ x e. A ) -> ( f " x ) ~< ( card ` T ) )
69 36 30 syl 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> ( cf ` ( card ` T ) ) = ( card ` T ) )
70 69 adantr 
 |-  ( ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) /\ x e. A ) -> ( cf ` ( card ` T ) ) = ( card ` T ) )
71 68 70 breqtrrd 
 |-  ( ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) /\ x e. A ) -> ( f " x ) ~< ( cf ` ( card ` T ) ) )
72 sseq1 
 |-  ( y = ( f " x ) -> ( y C_ ( card ` T ) <-> ( f " x ) C_ ( card ` T ) ) )
73 breq1 
 |-  ( y = ( f " x ) -> ( y ~< ( cf ` ( card ` T ) ) <-> ( f " x ) ~< ( cf ` ( card ` T ) ) ) )
74 72 73 anbi12d 
 |-  ( y = ( f " x ) -> ( ( y C_ ( card ` T ) /\ y ~< ( cf ` ( card ` T ) ) ) <-> ( ( f " x ) C_ ( card ` T ) /\ ( f " x ) ~< ( cf ` ( card ` T ) ) ) ) )
75 74 biimprcd 
 |-  ( ( ( f " x ) C_ ( card ` T ) /\ ( f " x ) ~< ( cf ` ( card ` T ) ) ) -> ( y = ( f " x ) -> ( y C_ ( card ` T ) /\ y ~< ( cf ` ( card ` T ) ) ) ) )
76 49 71 75 syl2anc 
 |-  ( ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) /\ x e. A ) -> ( y = ( f " x ) -> ( y C_ ( card ` T ) /\ y ~< ( cf ` ( card ` T ) ) ) ) )
77 76 rexlimdva 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> ( E. x e. A y = ( f " x ) -> ( y C_ ( card ` T ) /\ y ~< ( cf ` ( card ` T ) ) ) ) )
78 43 77 syl5bi 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> ( y e. { z | E. x e. A z = ( f " x ) } -> ( y C_ ( card ` T ) /\ y ~< ( cf ` ( card ` T ) ) ) ) )
79 78 ralrimiv 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> A. y e. { z | E. x e. A z = ( f " x ) } ( y C_ ( card ` T ) /\ y ~< ( cf ` ( card ` T ) ) ) )
80 fvex 
 |-  ( card ` T ) e. _V
81 80 cfslb2n 
 |-  ( ( Lim ( card ` T ) /\ A. y e. { z | E. x e. A z = ( f " x ) } ( y C_ ( card ` T ) /\ y ~< ( cf ` ( card ` T ) ) ) ) -> ( { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) -> U. { z | E. x e. A z = ( f " x ) } =/= ( card ` T ) ) )
82 39 79 81 syl2anc 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> ( { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) -> U. { z | E. x e. A z = ( f " x ) } =/= ( card ` T ) ) )
83 34 82 mpd 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> U. { z | E. x e. A z = ( f " x ) } =/= ( card ` T ) )
84 15 dfiun2 
 |-  U_ x e. A ( f " x ) = U. { z | E. x e. A z = ( f " x ) }
85 48 ralrimivw 
 |-  ( f : U. A -1-1-onto-> ( card ` T ) -> A. x e. A ( f " x ) C_ ( card ` T ) )
86 iunss 
 |-  ( U_ x e. A ( f " x ) C_ ( card ` T ) <-> A. x e. A ( f " x ) C_ ( card ` T ) )
87 85 86 sylibr 
 |-  ( f : U. A -1-1-onto-> ( card ` T ) -> U_ x e. A ( f " x ) C_ ( card ` T ) )
88 fof 
 |-  ( f : U. A -onto-> ( card ` T ) -> f : U. A --> ( card ` T ) )
89 foelrn 
 |-  ( ( f : U. A -onto-> ( card ` T ) /\ y e. ( card ` T ) ) -> E. z e. U. A y = ( f ` z ) )
90 89 ex 
 |-  ( f : U. A -onto-> ( card ` T ) -> ( y e. ( card ` T ) -> E. z e. U. A y = ( f ` z ) ) )
91 eluni2 
 |-  ( z e. U. A <-> E. x e. A z e. x )
92 nfv 
 |-  F/ x f : U. A --> ( card ` T )
93 nfiu1 
 |-  F/_ x U_ x e. A ( f " x )
94 93 nfel2 
 |-  F/ x ( f ` z ) e. U_ x e. A ( f " x )
95 ssiun2 
 |-  ( x e. A -> ( f " x ) C_ U_ x e. A ( f " x ) )
96 95 3ad2ant2 
 |-  ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f " x ) C_ U_ x e. A ( f " x ) )
97 ffn 
 |-  ( f : U. A --> ( card ` T ) -> f Fn U. A )
98 97 3ad2ant1 
 |-  ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> f Fn U. A )
99 51 3ad2ant2 
 |-  ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> x C_ U. A )
100 simp3 
 |-  ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> z e. x )
101 fnfvima 
 |-  ( ( f Fn U. A /\ x C_ U. A /\ z e. x ) -> ( f ` z ) e. ( f " x ) )
102 98 99 100 101 syl3anc 
 |-  ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f ` z ) e. ( f " x ) )
103 96 102 sseldd 
 |-  ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f ` z ) e. U_ x e. A ( f " x ) )
104 103 3exp 
 |-  ( f : U. A --> ( card ` T ) -> ( x e. A -> ( z e. x -> ( f ` z ) e. U_ x e. A ( f " x ) ) ) )
105 92 94 104 rexlimd 
 |-  ( f : U. A --> ( card ` T ) -> ( E. x e. A z e. x -> ( f ` z ) e. U_ x e. A ( f " x ) ) )
106 91 105 syl5bi 
 |-  ( f : U. A --> ( card ` T ) -> ( z e. U. A -> ( f ` z ) e. U_ x e. A ( f " x ) ) )
107 eleq1a 
 |-  ( ( f ` z ) e. U_ x e. A ( f " x ) -> ( y = ( f ` z ) -> y e. U_ x e. A ( f " x ) ) )
108 106 107 syl6 
 |-  ( f : U. A --> ( card ` T ) -> ( z e. U. A -> ( y = ( f ` z ) -> y e. U_ x e. A ( f " x ) ) ) )
109 108 rexlimdv 
 |-  ( f : U. A --> ( card ` T ) -> ( E. z e. U. A y = ( f ` z ) -> y e. U_ x e. A ( f " x ) ) )
110 88 90 109 sylsyld 
 |-  ( f : U. A -onto-> ( card ` T ) -> ( y e. ( card ` T ) -> y e. U_ x e. A ( f " x ) ) )
111 45 110 syl 
 |-  ( f : U. A -1-1-onto-> ( card ` T ) -> ( y e. ( card ` T ) -> y e. U_ x e. A ( f " x ) ) )
112 111 ssrdv 
 |-  ( f : U. A -1-1-onto-> ( card ` T ) -> ( card ` T ) C_ U_ x e. A ( f " x ) )
113 87 112 eqssd 
 |-  ( f : U. A -1-1-onto-> ( card ` T ) -> U_ x e. A ( f " x ) = ( card ` T ) )
114 84 113 eqtr3id 
 |-  ( f : U. A -1-1-onto-> ( card ` T ) -> U. { z | E. x e. A z = ( f " x ) } = ( card ` T ) )
115 114 necon3ai 
 |-  ( U. { z | E. x e. A z = ( f " x ) } =/= ( card ` T ) -> -. f : U. A -1-1-onto-> ( card ` T ) )
116 83 115 syl 
 |-  ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> -. f : U. A -1-1-onto-> ( card ` T ) )
117 116 pm2.01da 
 |-  ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. f : U. A -1-1-onto-> ( card ` T ) )
118 117 nexdv 
 |-  ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. E. f f : U. A -1-1-onto-> ( card ` T ) )
119 entr 
 |-  ( ( U. A ~~ T /\ T ~~ ( card ` T ) ) -> U. A ~~ ( card ` T ) )
120 3 119 sylan2 
 |-  ( ( U. A ~~ T /\ T e. Tarski ) -> U. A ~~ ( card ` T ) )
121 bren 
 |-  ( U. A ~~ ( card ` T ) <-> E. f f : U. A -1-1-onto-> ( card ` T ) )
122 120 121 sylib 
 |-  ( ( U. A ~~ T /\ T e. Tarski ) -> E. f f : U. A -1-1-onto-> ( card ` T ) )
123 122 expcom 
 |-  ( T e. Tarski -> ( U. A ~~ T -> E. f f : U. A -1-1-onto-> ( card ` T ) ) )
124 123 3ad2ant1 
 |-  ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( U. A ~~ T -> E. f f : U. A -1-1-onto-> ( card ` T ) ) )
125 118 124 mtod 
 |-  ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. U. A ~~ T )
126 uniss 
 |-  ( A C_ T -> U. A C_ U. T )
127 df-tr 
 |-  ( Tr T <-> U. T C_ T )
128 127 biimpi 
 |-  ( Tr T -> U. T C_ T )
129 126 128 sylan9ss 
 |-  ( ( A C_ T /\ Tr T ) -> U. A C_ T )
130 129 expcom 
 |-  ( Tr T -> ( A C_ T -> U. A C_ T ) )
131 57 130 syld 
 |-  ( Tr T -> ( A e. T -> U. A C_ T ) )
132 131 imp 
 |-  ( ( Tr T /\ A e. T ) -> U. A C_ T )
133 tsken 
 |-  ( ( T e. Tarski /\ U. A C_ T ) -> ( U. A ~~ T \/ U. A e. T ) )
134 132 133 sylan2 
 |-  ( ( T e. Tarski /\ ( Tr T /\ A e. T ) ) -> ( U. A ~~ T \/ U. A e. T ) )
135 134 3impb 
 |-  ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( U. A ~~ T \/ U. A e. T ) )
136 135 ord 
 |-  ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( -. U. A ~~ T -> U. A e. T ) )
137 125 136 mpd 
 |-  ( ( T e. Tarski /\ Tr T /\ A e. T ) -> U. A e. T )