Theorem tskuni 9072

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

Assertion

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

Proof of Theorem tskuni

Dummy variables f x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tsksdom 9045	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ A e. T ) -> A ~< T )
2		cardidg 8836	. . . . . . . . . . . . . 14 |- ( T e. Tarski -> ( card ` T ) ~~ T )
3	2	ensymd 7485	. . . . . . . . . . . . 13 |- ( T e. Tarski -> T ~~ ( card ` T ) )
4	3	adantr 463	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ A e. T ) -> T ~~ ( card ` T ) )
5		sdomentr 7570	. . . . . . . . . . . 12 |- ( ( A ~< T /\ T ~~ ( card ` T ) ) -> A ~< ( card ` T ) )
6	1, 4, 5	syl2anc 659	. . . . . . . . . . 11 |- ( ( T e. Tarski /\ A e. T ) -> A ~< ( card ` T ) )
7		eqid 2382	. . . . . . . . . . . . . . 15 |- ( x e. A |-> ( f " x ) ) = ( x e. A |-> ( f " x ) )
8	7	rnmpt 5161	. . . . . . . . . . . . . 14 |- ran ( x e. A |-> ( f " x ) ) = { z | E. x e. A z = ( f " x ) }
9		cardon 8238	. . . . . . . . . . . . . . . . 17 |- ( card ` T ) e. On
10		sdomdom 7462	. . . . . . . . . . . . . . . . 17 |- ( A ~< ( card ` T ) -> A ~<_ ( card ` T ) )
11		ondomen 8331	. . . . . . . . . . . . . . . . 17 |- ( ( ( card ` T ) e. On /\ A ~<_ ( card ` T ) ) -> A e. dom card )
12	9, 10, 11	sylancr 661	. . . . . . . . . . . . . . . 16 |- ( A ~< ( card ` T ) -> A e. dom card )
13	12	adantl 464	. . . . . . . . . . . . . . 15 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> A e. dom card )
14		vex 3037	. . . . . . . . . . . . . . . . . 18 |- f e. _V
15		imaexg 6636	. . . . . . . . . . . . . . . . . 18 |- ( f e. _V -> ( f " x ) e. _V )
16	14, 15	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( f " x ) e. _V
17	16, 7	fnmpti 5617	. . . . . . . . . . . . . . . 16 |- ( x e. A |-> ( f " x ) ) Fn A
18		dffn4 5709	. . . . . . . . . . . . . . . 16 |- ( ( x e. A |-> ( f " x ) ) Fn A <-> ( x e. A |-> ( f " x ) ) : A -onto-> ran ( x e. A |-> ( f " x ) ) )
19	17, 18	mpbi 208	. . . . . . . . . . . . . . 15 |- ( x e. A |-> ( f " x ) ) : A -onto-> ran ( x e. A |-> ( f " x ) )
20		fodomnum 8351	. . . . . . . . . . . . . . 15 |- ( A e. dom card -> ( ( x e. A |-> ( f " x ) ) : A -onto-> ran ( x e. A |-> ( f " x ) ) -> ran ( x e. A |-> ( f " x ) ) ~<_ A ) )
21	13, 19, 20	mpisyl 18	. . . . . . . . . . . . . 14 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> ran ( x e. A |-> ( f " x ) ) ~<_ A )
22	8, 21	syl5eqbrr 4401	. . . . . . . . . . . . 13 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~<_ A )
23		domsdomtr 7571	. . . . . . . . . . . . 13 |- ( ( { z | E. x e. A z = ( f " x ) } ~<_ A /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
24	22, 23	sylancom 665	. . . . . . . . . . . 12 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
25	24	adantll 711	. . . . . . . . . . 11 |- ( ( ( T e. Tarski /\ A e. T ) /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
26	6, 25	mpdan 666	. . . . . . . . . 10 |- ( ( T e. Tarski /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
27		ne0i 3717	. . . . . . . . . . . 12 |- ( A e. T -> T =/= (/) )
28		tskcard 9070	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ T =/= (/) ) -> ( card ` T ) e. Inacc )
29	27, 28	sylan2 472	. . . . . . . . . . 11 |- ( ( T e. Tarski /\ A e. T ) -> ( card ` T ) e. Inacc )
30		elina 8976	. . . . . . . . . . . 12 |- ( ( card ` T ) e. Inacc <-> ( ( card ` T ) =/= (/) /\ ( cf ` ( card ` T ) ) = ( card ` T ) /\ A. x e. ( card ` T ) ~P x ~< ( card ` T ) ) )
31	30	simp2bi 1010	. . . . . . . . . . 11 |- ( ( card ` T ) e. Inacc -> ( cf ` ( card ` T ) ) = ( card ` T ) )
32	29, 31	syl 16	. . . . . . . . . 10 |- ( ( T e. Tarski /\ A e. T ) -> ( cf ` ( card ` T ) ) = ( card ` T ) )
33	26, 32	breqtrrd 4393	. . . . . . . . 9 |- ( ( T e. Tarski /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) )
34	33	3adant2 1013	. . . . . . . 8 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) )
35	34	adantr 463	. . . . . . 7 |- ( ( ( 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 ) ) )
36	29	3adant2 1013	. . . . . . . . . 10 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( card ` T ) e. Inacc )
37	36	adantr 463	. . . . . . . . 9 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> ( card ` T ) e. Inacc )
38		inawina 8979	. . . . . . . . 9 |- ( ( card ` T ) e. Inacc -> ( card ` T ) e. InaccW )
39		winalim 8984	. . . . . . . . 9 |- ( ( card ` T ) e. InaccW -> Lim ( card ` T ) )
40	37, 38, 39	3syl 20	. . . . . . . 8 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> Lim ( card ` T ) )
41		vex 3037	. . . . . . . . . . 11 |- y e. _V
42		eqeq1 2386	. . . . . . . . . . . 12 |- ( z = y -> ( z = ( f " x ) <-> y = ( f " x ) ) )
43	42	rexbidv 2893	. . . . . . . . . . 11 |- ( z = y -> ( E. x e. A z = ( f " x ) <-> E. x e. A y = ( f " x ) ) )
44	41, 43	elab 3171	. . . . . . . . . 10 |- ( y e. { z | E. x e. A z = ( f " x ) } <-> E. x e. A y = ( f " x ) )
45		imassrn 5260	. . . . . . . . . . . . . 14 |- ( f " x ) C_ ran f
46		f1ofo 5731	. . . . . . . . . . . . . . 15 |- ( f : U. A -1-1-onto-> ( card ` T ) -> f : U. A -onto-> ( card ` T ) )
47		forn 5706	. . . . . . . . . . . . . . 15 |- ( f : U. A -onto-> ( card ` T ) -> ran f = ( card ` T ) )
48	46, 47	syl 16	. . . . . . . . . . . . . 14 |- ( f : U. A -1-1-onto-> ( card ` T ) -> ran f = ( card ` T ) )
49	45, 48	syl5sseq 3465	. . . . . . . . . . . . 13 |- ( f : U. A -1-1-onto-> ( card ` T ) -> ( f " x ) C_ ( card ` T ) )
50	49	ad2antlr 724	. . . . . . . . . . . 12 |- ( ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) /\ x e. A ) -> ( f " x ) C_ ( card ` T ) )
51		f1of1 5723	. . . . . . . . . . . . . . . 16 |- ( f : U. A -1-1-onto-> ( card ` T ) -> f : U. A -1-1-> ( card ` T ) )
52		elssuni 4192	. . . . . . . . . . . . . . . 16 |- ( x e. A -> x C_ U. A )
53		vex 3037	. . . . . . . . . . . . . . . . 17 |- x e. _V
54	53	f1imaen 7496	. . . . . . . . . . . . . . . 16 |- ( ( f : U. A -1-1-> ( card ` T ) /\ x C_ U. A ) -> ( f " x ) ~~ x )
55	51, 52, 54	syl2an 475	. . . . . . . . . . . . . . 15 |- ( ( f : U. A -1-1-onto-> ( card ` T ) /\ x e. A ) -> ( f " x ) ~~ x )
56	55	adantll 711	. . . . . . . . . . . . . 14 |- ( ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) /\ x e. A ) -> ( f " x ) ~~ x )
57		simpl1 997	. . . . . . . . . . . . . . . . 17 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> T e. Tarski )
58		trss 4469	. . . . . . . . . . . . . . . . . . . 20 |- ( Tr T -> ( A e. T -> A C_ T ) )
59	58	imp 427	. . . . . . . . . . . . . . . . . . 19 |- ( ( Tr T /\ A e. T ) -> A C_ T )
60	59	3adant1 1012	. . . . . . . . . . . . . . . . . 18 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> A C_ T )
61	60	sselda 3417	. . . . . . . . . . . . . . . . 17 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x e. T )
62		tsksdom 9045	. . . . . . . . . . . . . . . . 17 |- ( ( T e. Tarski /\ x e. T ) -> x ~< T )
63	57, 61, 62	syl2anc 659	. . . . . . . . . . . . . . . 16 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x ~< T )
64	57, 3	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> T ~~ ( card ` T ) )
65		sdomentr 7570	. . . . . . . . . . . . . . . 16 |- ( ( x ~< T /\ T ~~ ( card ` T ) ) -> x ~< ( card ` T ) )
66	63, 64, 65	syl2anc 659	. . . . . . . . . . . . . . 15 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x ~< ( card ` T ) )
67	66	adantlr 712	. . . . . . . . . . . . . 14 |- ( ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) /\ x e. A ) -> x ~< ( card ` T ) )
68		ensdomtr 7572	. . . . . . . . . . . . . 14 |- ( ( ( f " x ) ~~ x /\ x ~< ( card ` T ) ) -> ( f " x ) ~< ( card ` T ) )
69	56, 67, 68	syl2anc 659	. . . . . . . . . . . . 13 |- ( ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) /\ x e. A ) -> ( f " x ) ~< ( card ` T ) )
70	37, 31	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> ( cf ` ( card ` T ) ) = ( card ` T ) )
71	70	adantr 463	. . . . . . . . . . . . 13 |- ( ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) /\ x e. A ) -> ( cf ` ( card ` T ) ) = ( card ` T ) )
72	69, 71	breqtrrd 4393	. . . . . . . . . . . 12 |- ( ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) /\ x e. A ) -> ( f " x ) ~< ( cf ` ( card ` T ) ) )
73		sseq1 3438	. . . . . . . . . . . . . 14 |- ( y = ( f " x ) -> ( y C_ ( card ` T ) <-> ( f " x ) C_ ( card ` T ) ) )
74		breq1 4370	. . . . . . . . . . . . . 14 |- ( y = ( f " x ) -> ( y ~< ( cf ` ( card ` T ) ) <-> ( f " x ) ~< ( cf ` ( card ` T ) ) ) )
75	73, 74	anbi12d 708	. . . . . . . . . . . . 13 |- ( y = ( f " x ) -> ( ( y C_ ( card ` T ) /\ y ~< ( cf ` ( card ` T ) ) ) <-> ( ( f " x ) C_ ( card ` T ) /\ ( f " x ) ~< ( cf ` ( card ` T ) ) ) ) )
76	75	biimprcd 225	. . . . . . . . . . . 12 |- ( ( ( f " x ) C_ ( card ` T ) /\ ( f " x ) ~< ( cf ` ( card ` T ) ) ) -> ( y = ( f " x ) -> ( y C_ ( card ` T ) /\ y ~< ( cf ` ( card ` T ) ) ) ) )
77	50, 72, 76	syl2anc 659	. . . . . . . . . . 11 |- ( ( ( ( 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 ) ) ) ) )
78	77	rexlimdva 2874	. . . . . . . . . 10 |- ( ( ( 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 ) ) ) ) )
79	44, 78	syl5bi 217	. . . . . . . . 9 |- ( ( ( 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 ) ) ) ) )
80	79	ralrimiv 2794	. . . . . . . 8 |- ( ( ( 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 ) ) ) )
81		fvex 5784	. . . . . . . . 9 |- ( card ` T ) e. _V
82	81	cfslb2n 8561	. . . . . . . 8 |- ( ( 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 ) ) )
83	40, 80, 82	syl2anc 659	. . . . . . 7 |- ( ( ( 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 ) ) )
84	35, 83	mpd 15	. . . . . 6 |- ( ( ( 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 ) )
85	16	dfiun2 4277	. . . . . . . 8 |- U_ x e. A ( f " x ) = U. { z | E. x e. A z = ( f " x ) }
86	49	ralrimivw 2797	. . . . . . . . . 10 |- ( f : U. A -1-1-onto-> ( card ` T ) -> A. x e. A ( f " x ) C_ ( card ` T ) )
87		iunss 4284	. . . . . . . . . 10 |- ( U_ x e. A ( f " x ) C_ ( card ` T ) <-> A. x e. A ( f " x ) C_ ( card ` T ) )
88	86, 87	sylibr 212	. . . . . . . . 9 |- ( f : U. A -1-1-onto-> ( card ` T ) -> U_ x e. A ( f " x ) C_ ( card ` T ) )
89		fof 5703	. . . . . . . . . . . 12 |- ( f : U. A -onto-> ( card ` T ) -> f : U. A --> ( card ` T ) )
90		foelrn 5952	. . . . . . . . . . . . 13 |- ( ( f : U. A -onto-> ( card ` T ) /\ y e. ( card ` T ) ) -> E. z e. U. A y = ( f ` z ) )
91	90	ex 432	. . . . . . . . . . . 12 |- ( f : U. A -onto-> ( card ` T ) -> ( y e. ( card ` T ) -> E. z e. U. A y = ( f ` z ) ) )
92		eluni2 4167	. . . . . . . . . . . . . . 15 |- ( z e. U. A <-> E. x e. A z e. x )
93		nfv 1715	. . . . . . . . . . . . . . . 16 |- F/ x f : U. A --> ( card ` T )
94		nfiu1 4273	. . . . . . . . . . . . . . . . 17 |- F/_ x U_ x e. A ( f " x )
95	94	nfel2 2562	. . . . . . . . . . . . . . . 16 |- F/ x ( f ` z ) e. U_ x e. A ( f " x )
96		ssiun2 4286	. . . . . . . . . . . . . . . . . . 19 |- ( x e. A -> ( f " x ) C_ U_ x e. A ( f " x ) )
97	96	3ad2ant2 1016	. . . . . . . . . . . . . . . . . 18 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f " x ) C_ U_ x e. A ( f " x ) )
98		ffn 5639	. . . . . . . . . . . . . . . . . . . 20 |- ( f : U. A --> ( card ` T ) -> f Fn U. A )
99	98	3ad2ant1 1015	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> f Fn U. A )
100	52	3ad2ant2 1016	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> x C_ U. A )
101		simp3 996	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> z e. x )
102		fnfvima 6051	. . . . . . . . . . . . . . . . . . 19 |- ( ( f Fn U. A /\ x C_ U. A /\ z e. x ) -> ( f ` z ) e. ( f " x ) )
103	99, 100, 101, 102	syl3anc 1226	. . . . . . . . . . . . . . . . . 18 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f ` z ) e. ( f " x ) )
104	97, 103	sseldd 3418	. . . . . . . . . . . . . . . . 17 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f ` z ) e. U_ x e. A ( f " x ) )
105	104	3exp 1193	. . . . . . . . . . . . . . . 16 |- ( f : U. A --> ( card ` T ) -> ( x e. A -> ( z e. x -> ( f ` z ) e. U_ x e. A ( f " x ) ) ) )
106	93, 95, 105	rexlimd 2866	. . . . . . . . . . . . . . 15 |- ( f : U. A --> ( card ` T ) -> ( E. x e. A z e. x -> ( f ` z ) e. U_ x e. A ( f " x ) ) )
107	92, 106	syl5bi 217	. . . . . . . . . . . . . 14 |- ( f : U. A --> ( card ` T ) -> ( z e. U. A -> ( f ` z ) e. U_ x e. A ( f " x ) ) )
108		eleq1a 2465	. . . . . . . . . . . . . 14 |- ( ( f ` z ) e. U_ x e. A ( f " x ) -> ( y = ( f ` z ) -> y e. U_ x e. A ( f " x ) ) )
109	107, 108	syl6 33	. . . . . . . . . . . . 13 |- ( f : U. A --> ( card ` T ) -> ( z e. U. A -> ( y = ( f ` z ) -> y e. U_ x e. A ( f " x ) ) ) )
110	109	rexlimdv 2872	. . . . . . . . . . . 12 |- ( f : U. A --> ( card ` T ) -> ( E. z e. U. A y = ( f ` z ) -> y e. U_ x e. A ( f " x ) ) )
111	89, 91, 110	sylsyld 56	. . . . . . . . . . 11 |- ( f : U. A -onto-> ( card ` T ) -> ( y e. ( card ` T ) -> y e. U_ x e. A ( f " x ) ) )
112	46, 111	syl 16	. . . . . . . . . 10 |- ( f : U. A -1-1-onto-> ( card ` T ) -> ( y e. ( card ` T ) -> y e. U_ x e. A ( f " x ) ) )
113	112	ssrdv 3423	. . . . . . . . 9 |- ( f : U. A -1-1-onto-> ( card ` T ) -> ( card ` T ) C_ U_ x e. A ( f " x ) )
114	88, 113	eqssd 3434	. . . . . . . 8 |- ( f : U. A -1-1-onto-> ( card ` T ) -> U_ x e. A ( f " x ) = ( card ` T ) )
115	85, 114	syl5eqr 2437	. . . . . . 7 |- ( f : U. A -1-1-onto-> ( card ` T ) -> U. { z | E. x e. A z = ( f " x ) } = ( card ` T ) )
116	115	necon3ai 2610	. . . . . 6 |- ( U. { z | E. x e. A z = ( f " x ) } =/= ( card ` T ) -> -. f : U. A -1-1-onto-> ( card ` T ) )
117	84, 116	syl 16	. . . . 5 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> -. f : U. A -1-1-onto-> ( card ` T ) )
118	117	pm2.01da 440	. . . 4 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. f : U. A -1-1-onto-> ( card ` T ) )
119	118	nexdv 1892	. . 3 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. E. f f : U. A -1-1-onto-> ( card ` T ) )
120		entr 7486	. . . . . . 7 |- ( ( U. A ~~ T /\ T ~~ ( card ` T ) ) -> U. A ~~ ( card ` T ) )
121	3, 120	sylan2 472	. . . . . 6 |- ( ( U. A ~~ T /\ T e. Tarski ) -> U. A ~~ ( card ` T ) )
122		bren 7444	. . . . . 6 |- ( U. A ~~ ( card ` T ) <-> E. f f : U. A -1-1-onto-> ( card ` T ) )
123	121, 122	sylib 196	. . . . 5 |- ( ( U. A ~~ T /\ T e. Tarski ) -> E. f f : U. A -1-1-onto-> ( card ` T ) )
124	123	expcom 433	. . . 4 |- ( T e. Tarski -> ( U. A ~~ T -> E. f f : U. A -1-1-onto-> ( card ` T ) ) )
125	124	3ad2ant1 1015	. . 3 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( U. A ~~ T -> E. f f : U. A -1-1-onto-> ( card ` T ) ) )
126	119, 125	mtod 177	. 2 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. U. A ~~ T )
127		uniss 4184	. . . . . . . . 9 |- ( A C_ T -> U. A C_ U. T )
128		df-tr 4461	. . . . . . . . . 10 |- ( Tr T <-> U. T C_ T )
129	128	biimpi 194	. . . . . . . . 9 |- ( Tr T -> U. T C_ T )
130	127, 129	sylan9ss 3430	. . . . . . . 8 |- ( ( A C_ T /\ Tr T ) -> U. A C_ T )
131	130	expcom 433	. . . . . . 7 |- ( Tr T -> ( A C_ T -> U. A C_ T ) )
132	58, 131	syld 44	. . . . . 6 |- ( Tr T -> ( A e. T -> U. A C_ T ) )
133	132	imp 427	. . . . 5 |- ( ( Tr T /\ A e. T ) -> U. A C_ T )
134		tsken 9043	. . . . 5 |- ( ( T e. Tarski /\ U. A C_ T ) -> ( U. A ~~ T \/ U. A e. T ) )
135	133, 134	sylan2 472	. . . 4 |- ( ( T e. Tarski /\ ( Tr T /\ A e. T ) ) -> ( U. A ~~ T \/ U. A e. T ) )
136	135	3impb 1190	. . 3 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( U. A ~~ T \/ U. A e. T ) )
137	136	ord 375	. 2 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( -. U. A ~~ T -> U. A e. T ) )
138	126, 137	mpd 15	1 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> U. A e. T )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 366   /\ wa 367   /\ w3a 971   = wceq 1399   E.wex 1620   e. wcel 1826   {cab 2367   =/= wne 2577   A.wral 2732   E.wrex 2733   _Vcvv 3034   C_ wss 3389   (/)c0 3711   ~Pcpw 3927   U.cuni 4163   U_ciun 4243   class class class wbr 4367   |-> cmpt 4425   Tr wtr 4460   Oncon0 4792   Lim wlim 4793   dom cdm 4913   ran crn 4914   "cima 4916   Fn wfn 5491   -->wf 5492   -1-1->wf1 5493   -onto->wfo 5494   -1-1-onto->wf1o 5495   ` cfv 5496   ~~ cen 7432   ~<_ cdom 7433   ~< csdm 7434   cardccrd 8229   cfccf 8231   InaccWcwina 8971   Inacccina 8972   Tarskictsk 9037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-rep 4478  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-inf2 7972  ax-ac2 8756

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-reu 2739  df-rmo 2740  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-int 4200  df-iun 4245  df-iin 4246  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-se 4753  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-isom 5505  df-riota 6158  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-om 6600  df-1st 6699  df-2nd 6700  df-smo 6935  df-recs 6960  df-rdg 6994  df-1o 7048  df-2o 7049  df-oadd 7052  df-er 7229  df-map 7340  df-ixp 7389  df-en 7436  df-dom 7437  df-sdom 7438  df-fin 7439  df-oi 7850  df-har 7899  df-r1 8095  df-card 8233  df-aleph 8234  df-cf 8235  df-acn 8236  df-ac 8410  df-wina 8973  df-ina 8974  df-tsk 9038

This theorem is referenced by:  tskwun  9073  tskint  9074  tskun  9075  tskurn  9078  pwinfi3  38177