Theorem tskuni 9234

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 9207	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ A e. T ) -> A ~< T )
2		cardidg 8999	. . . . . . . . . . . . . 14 |- ( T e. Tarski -> ( card ` T ) ~~ T )
3	2	ensymd 7646	. . . . . . . . . . . . 13 |- ( T e. Tarski -> T ~~ ( card ` T ) )
4	3	adantr 471	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ A e. T ) -> T ~~ ( card ` T ) )
5		sdomentr 7732	. . . . . . . . . . . 12 |- ( ( A ~< T /\ T ~~ ( card ` T ) ) -> A ~< ( card ` T ) )
6	1, 4, 5	syl2anc 671	. . . . . . . . . . 11 |- ( ( T e. Tarski /\ A e. T ) -> A ~< ( card ` T ) )
7		eqid 2462	. . . . . . . . . . . . . . 15 |- ( x e. A |-> ( f " x ) ) = ( x e. A |-> ( f " x ) )
8	7	rnmpt 5099	. . . . . . . . . . . . . 14 |- ran ( x e. A |-> ( f " x ) ) = { z | E. x e. A z = ( f " x ) }
9		cardon 8404	. . . . . . . . . . . . . . . . 17 |- ( card ` T ) e. On
10		sdomdom 7623	. . . . . . . . . . . . . . . . 17 |- ( A ~< ( card ` T ) -> A ~<_ ( card ` T ) )
11		ondomen 8494	. . . . . . . . . . . . . . . . 17 |- ( ( ( card ` T ) e. On /\ A ~<_ ( card ` T ) ) -> A e. dom card )
12	9, 10, 11	sylancr 674	. . . . . . . . . . . . . . . 16 |- ( A ~< ( card ` T ) -> A e. dom card )
13	12	adantl 472	. . . . . . . . . . . . . . 15 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> A e. dom card )
14		vex 3060	. . . . . . . . . . . . . . . . . 18 |- f e. _V
15		imaexg 6757	. . . . . . . . . . . . . . . . . 18 |- ( f e. _V -> ( f " x ) e. _V )
16	14, 15	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( f " x ) e. _V
17	16, 7	fnmpti 5728	. . . . . . . . . . . . . . . 16 |- ( x e. A |-> ( f " x ) ) Fn A
18		dffn4 5822	. . . . . . . . . . . . . . . 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 213	. . . . . . . . . . . . . . 15 |- ( x e. A |-> ( f " x ) ) : A -onto-> ran ( x e. A |-> ( f " x ) )
20		fodomnum 8514	. . . . . . . . . . . . . . 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 21	. . . . . . . . . . . . . 14 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> ran ( x e. A |-> ( f " x ) ) ~<_ A )
22	8, 21	syl5eqbrr 4451	. . . . . . . . . . . . 13 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~<_ A )
23		domsdomtr 7733	. . . . . . . . . . . . 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 678	. . . . . . . . . . . 12 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
25	24	adantll 725	. . . . . . . . . . 11 |- ( ( ( T e. Tarski /\ A e. T ) /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
26	6, 25	mpdan 679	. . . . . . . . . 10 |- ( ( T e. Tarski /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
27		ne0i 3749	. . . . . . . . . . . 12 |- ( A e. T -> T =/= (/) )
28		tskcard 9232	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ T =/= (/) ) -> ( card ` T ) e. Inacc )
29	27, 28	sylan2 481	. . . . . . . . . . 11 |- ( ( T e. Tarski /\ A e. T ) -> ( card ` T ) e. Inacc )
30		elina 9138	. . . . . . . . . . . 12 |- ( ( card ` T ) e. Inacc <-> ( ( card ` T ) =/= (/) /\ ( cf ` ( card ` T ) ) = ( card ` T ) /\ A. x e. ( card ` T ) ~P x ~< ( card ` T ) ) )
31	30	simp2bi 1030	. . . . . . . . . . 11 |- ( ( card ` T ) e. Inacc -> ( cf ` ( card ` T ) ) = ( card ` T ) )
32	29, 31	syl 17	. . . . . . . . . 10 |- ( ( T e. Tarski /\ A e. T ) -> ( cf ` ( card ` T ) ) = ( card ` T ) )
33	26, 32	breqtrrd 4443	. . . . . . . . 9 |- ( ( T e. Tarski /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) )
34	33	3adant2 1033	. . . . . . . 8 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) )
35	34	adantr 471	. . . . . . 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 1033	. . . . . . . . . 10 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( card ` T ) e. Inacc )
37	36	adantr 471	. . . . . . . . 9 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> ( card ` T ) e. Inacc )
38		inawina 9141	. . . . . . . . 9 |- ( ( card ` T ) e. Inacc -> ( card ` T ) e. InaccW )
39		winalim 9146	. . . . . . . . 9 |- ( ( card ` T ) e. InaccW -> Lim ( card ` T ) )
40	37, 38, 39	3syl 18	. . . . . . . 8 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> Lim ( card ` T ) )
41		vex 3060	. . . . . . . . . . 11 |- y e. _V
42		eqeq1 2466	. . . . . . . . . . . 12 |- ( z = y -> ( z = ( f " x ) <-> y = ( f " x ) ) )
43	42	rexbidv 2913	. . . . . . . . . . 11 |- ( z = y -> ( E. x e. A z = ( f " x ) <-> E. x e. A y = ( f " x ) ) )
44	41, 43	elab 3197	. . . . . . . . . 10 |- ( y e. { z | E. x e. A z = ( f " x ) } <-> E. x e. A y = ( f " x ) )
45		imassrn 5198	. . . . . . . . . . . . . 14 |- ( f " x ) C_ ran f
46		f1ofo 5844	. . . . . . . . . . . . . . 15 |- ( f : U. A -1-1-onto-> ( card ` T ) -> f : U. A -onto-> ( card ` T ) )
47		forn 5819	. . . . . . . . . . . . . . 15 |- ( f : U. A -onto-> ( card ` T ) -> ran f = ( card ` T ) )
48	46, 47	syl 17	. . . . . . . . . . . . . 14 |- ( f : U. A -1-1-onto-> ( card ` T ) -> ran f = ( card ` T ) )
49	45, 48	syl5sseq 3492	. . . . . . . . . . . . 13 |- ( f : U. A -1-1-onto-> ( card ` T ) -> ( f " x ) C_ ( card ` T ) )
50	49	ad2antlr 738	. . . . . . . . . . . 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 5836	. . . . . . . . . . . . . . . 16 |- ( f : U. A -1-1-onto-> ( card ` T ) -> f : U. A -1-1-> ( card ` T ) )
52		elssuni 4241	. . . . . . . . . . . . . . . 16 |- ( x e. A -> x C_ U. A )
53		vex 3060	. . . . . . . . . . . . . . . . 17 |- x e. _V
54	53	f1imaen 7657	. . . . . . . . . . . . . . . 16 |- ( ( f : U. A -1-1-> ( card ` T ) /\ x C_ U. A ) -> ( f " x ) ~~ x )
55	51, 52, 54	syl2an 484	. . . . . . . . . . . . . . 15 |- ( ( f : U. A -1-1-onto-> ( card ` T ) /\ x e. A ) -> ( f " x ) ~~ x )
56	55	adantll 725	. . . . . . . . . . . . . 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 1017	. . . . . . . . . . . . . . . . 17 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> T e. Tarski )
58		trss 4520	. . . . . . . . . . . . . . . . . . . 20 |- ( Tr T -> ( A e. T -> A C_ T ) )
59	58	imp 435	. . . . . . . . . . . . . . . . . . 19 |- ( ( Tr T /\ A e. T ) -> A C_ T )
60	59	3adant1 1032	. . . . . . . . . . . . . . . . . 18 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> A C_ T )
61	60	sselda 3444	. . . . . . . . . . . . . . . . 17 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x e. T )
62		tsksdom 9207	. . . . . . . . . . . . . . . . 17 |- ( ( T e. Tarski /\ x e. T ) -> x ~< T )
63	57, 61, 62	syl2anc 671	. . . . . . . . . . . . . . . 16 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x ~< T )
64	57, 3	syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> T ~~ ( card ` T ) )
65		sdomentr 7732	. . . . . . . . . . . . . . . 16 |- ( ( x ~< T /\ T ~~ ( card ` T ) ) -> x ~< ( card ` T ) )
66	63, 64, 65	syl2anc 671	. . . . . . . . . . . . . . 15 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x ~< ( card ` T ) )
67	66	adantlr 726	. . . . . . . . . . . . . 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 7734	. . . . . . . . . . . . . 14 |- ( ( ( f " x ) ~~ x /\ x ~< ( card ` T ) ) -> ( f " x ) ~< ( card ` T ) )
69	56, 67, 68	syl2anc 671	. . . . . . . . . . . . 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 17	. . . . . . . . . . . . . 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 471	. . . . . . . . . . . . 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 4443	. . . . . . . . . . . 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 3465	. . . . . . . . . . . . . 14 |- ( y = ( f " x ) -> ( y C_ ( card ` T ) <-> ( f " x ) C_ ( card ` T ) ) )
74		breq1 4419	. . . . . . . . . . . . . 14 |- ( y = ( f " x ) -> ( y ~< ( cf ` ( card ` T ) ) <-> ( f " x ) ~< ( cf ` ( card ` T ) ) ) )
75	73, 74	anbi12d 722	. . . . . . . . . . . . 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 233	. . . . . . . . . . . 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 671	. . . . . . . . . . 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 2891	. . . . . . . . . 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 225	. . . . . . . . 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 2812	. . . . . . . 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 5898	. . . . . . . . 9 |- ( card ` T ) e. _V
82	81	cfslb2n 8724	. . . . . . . 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 671	. . . . . . 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 4326	. . . . . . . 8 |- U_ x e. A ( f " x ) = U. { z | E. x e. A z = ( f " x ) }
86	49	ralrimivw 2815	. . . . . . . . . 10 |- ( f : U. A -1-1-onto-> ( card ` T ) -> A. x e. A ( f " x ) C_ ( card ` T ) )
87		iunss 4333	. . . . . . . . . 10 |- ( U_ x e. A ( f " x ) C_ ( card ` T ) <-> A. x e. A ( f " x ) C_ ( card ` T ) )
88	86, 87	sylibr 217	. . . . . . . . 9 |- ( f : U. A -1-1-onto-> ( card ` T ) -> U_ x e. A ( f " x ) C_ ( card ` T ) )
89		fof 5816	. . . . . . . . . . . 12 |- ( f : U. A -onto-> ( card ` T ) -> f : U. A --> ( card ` T ) )
90		foelrn 6064	. . . . . . . . . . . . 13 |- ( ( f : U. A -onto-> ( card ` T ) /\ y e. ( card ` T ) ) -> E. z e. U. A y = ( f ` z ) )
91	90	ex 440	. . . . . . . . . . . 12 |- ( f : U. A -onto-> ( card ` T ) -> ( y e. ( card ` T ) -> E. z e. U. A y = ( f ` z ) ) )
92		eluni2 4216	. . . . . . . . . . . . . . 15 |- ( z e. U. A <-> E. x e. A z e. x )
93		nfv 1772	. . . . . . . . . . . . . . . 16 |- F/ x f : U. A --> ( card ` T )
94		nfiu1 4322	. . . . . . . . . . . . . . . . 17 |- F/_ x U_ x e. A ( f " x )
95	94	nfel2 2619	. . . . . . . . . . . . . . . 16 |- F/ x ( f ` z ) e. U_ x e. A ( f " x )
96		ssiun2 4335	. . . . . . . . . . . . . . . . . . 19 |- ( x e. A -> ( f " x ) C_ U_ x e. A ( f " x ) )
97	96	3ad2ant2 1036	. . . . . . . . . . . . . . . . . 18 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f " x ) C_ U_ x e. A ( f " x ) )
98		ffn 5751	. . . . . . . . . . . . . . . . . . . 20 |- ( f : U. A --> ( card ` T ) -> f Fn U. A )
99	98	3ad2ant1 1035	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> f Fn U. A )
100	52	3ad2ant2 1036	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> x C_ U. A )
101		simp3 1016	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> z e. x )
102		fnfvima 6168	. . . . . . . . . . . . . . . . . . 19 |- ( ( f Fn U. A /\ x C_ U. A /\ z e. x ) -> ( f ` z ) e. ( f " x ) )
103	99, 100, 101, 102	syl3anc 1276	. . . . . . . . . . . . . . . . . 18 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f ` z ) e. ( f " x ) )
104	97, 103	sseldd 3445	. . . . . . . . . . . . . . . . 17 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f ` z ) e. U_ x e. A ( f " x ) )
105	104	3exp 1214	. . . . . . . . . . . . . . . 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 2883	. . . . . . . . . . . . . . 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 225	. . . . . . . . . . . . . 14 |- ( f : U. A --> ( card ` T ) -> ( z e. U. A -> ( f ` z ) e. U_ x e. A ( f " x ) ) )
108		eleq1a 2535	. . . . . . . . . . . . . 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 34	. . . . . . . . . . . . 13 |- ( f : U. A --> ( card ` T ) -> ( z e. U. A -> ( y = ( f ` z ) -> y e. U_ x e. A ( f " x ) ) ) )
110	109	rexlimdv 2889	. . . . . . . . . . . 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 58	. . . . . . . . . . 11 |- ( f : U. A -onto-> ( card ` T ) -> ( y e. ( card ` T ) -> y e. U_ x e. A ( f " x ) ) )
112	46, 111	syl 17	. . . . . . . . . 10 |- ( f : U. A -1-1-onto-> ( card ` T ) -> ( y e. ( card ` T ) -> y e. U_ x e. A ( f " x ) ) )
113	112	ssrdv 3450	. . . . . . . . 9 |- ( f : U. A -1-1-onto-> ( card ` T ) -> ( card ` T ) C_ U_ x e. A ( f " x ) )
114	88, 113	eqssd 3461	. . . . . . . 8 |- ( f : U. A -1-1-onto-> ( card ` T ) -> U_ x e. A ( f " x ) = ( card ` T ) )
115	85, 114	syl5eqr 2510	. . . . . . 7 |- ( f : U. A -1-1-onto-> ( card ` T ) -> U. { z | E. x e. A z = ( f " x ) } = ( card ` T ) )
116	115	necon3ai 2661	. . . . . 6 |- ( U. { z | E. x e. A z = ( f " x ) } =/= ( card ` T ) -> -. f : U. A -1-1-onto-> ( card ` T ) )
117	84, 116	syl 17	. . . . 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 448	. . . 4 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. f : U. A -1-1-onto-> ( card ` T ) )
119	118	nexdv 1793	. . 3 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. E. f f : U. A -1-1-onto-> ( card ` T ) )
120		entr 7647	. . . . . . 7 |- ( ( U. A ~~ T /\ T ~~ ( card ` T ) ) -> U. A ~~ ( card ` T ) )
121	3, 120	sylan2 481	. . . . . 6 |- ( ( U. A ~~ T /\ T e. Tarski ) -> U. A ~~ ( card ` T ) )
122		bren 7604	. . . . . 6 |- ( U. A ~~ ( card ` T ) <-> E. f f : U. A -1-1-onto-> ( card ` T ) )
123	121, 122	sylib 201	. . . . 5 |- ( ( U. A ~~ T /\ T e. Tarski ) -> E. f f : U. A -1-1-onto-> ( card ` T ) )
124	123	expcom 441	. . . 4 |- ( T e. Tarski -> ( U. A ~~ T -> E. f f : U. A -1-1-onto-> ( card ` T ) ) )
125	124	3ad2ant1 1035	. . 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 182	. 2 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. U. A ~~ T )
127		uniss 4233	. . . . . . . . 9 |- ( A C_ T -> U. A C_ U. T )
128		df-tr 4512	. . . . . . . . . 10 |- ( Tr T <-> U. T C_ T )
129	128	biimpi 199	. . . . . . . . 9 |- ( Tr T -> U. T C_ T )
130	127, 129	sylan9ss 3457	. . . . . . . 8 |- ( ( A C_ T /\ Tr T ) -> U. A C_ T )
131	130	expcom 441	. . . . . . 7 |- ( Tr T -> ( A C_ T -> U. A C_ T ) )
132	58, 131	syld 45	. . . . . 6 |- ( Tr T -> ( A e. T -> U. A C_ T ) )
133	132	imp 435	. . . . 5 |- ( ( Tr T /\ A e. T ) -> U. A C_ T )
134		tsken 9205	. . . . 5 |- ( ( T e. Tarski /\ U. A C_ T ) -> ( U. A ~~ T \/ U. A e. T ) )
135	133, 134	sylan2 481	. . . 4 |- ( ( T e. Tarski /\ ( Tr T /\ A e. T ) ) -> ( U. A ~~ T \/ U. A e. T ) )
136	135	3impb 1211	. . 3 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( U. A ~~ T \/ U. A e. T ) )
137	136	ord 383	. 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 374   /\ wa 375   /\ w3a 991   = wceq 1455   E.wex 1674   e. wcel 1898   {cab 2448   =/= wne 2633   A.wral 2749   E.wrex 2750   _Vcvv 3057   C_ wss 3416   (/)c0 3743   ~Pcpw 3963   U.cuni 4212   U_ciun 4292   class class class wbr 4416   |-> cmpt 4475   Tr wtr 4511   dom cdm 4853   ran crn 4854   "cima 4856   Oncon0 5442   Lim wlim 5443   Fn wfn 5596   -->wf 5597   -1-1->wf1 5598   -onto->wfo 5599   -1-1-onto->wf1o 5600   ` cfv 5601   ~~ cen 7592   ~<_ cdom 7593   ~< csdm 7594   cardccrd 8395   cfccf 8397   InaccWcwina 9133   Inacccina 9134   Tarskictsk 9199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-inf2 8172  ax-ac2 8919

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-smo 7091  df-recs 7116  df-rdg 7154  df-1o 7208  df-2o 7209  df-oadd 7212  df-er 7389  df-map 7500  df-ixp 7549  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-oi 8051  df-har 8099  df-r1 8261  df-card 8399  df-aleph 8400  df-cf 8401  df-acn 8402  df-ac 8573  df-wina 9135  df-ina 9136  df-tsk 9200

This theorem is referenced by:  tskwun  9235  tskint  9236  tskun  9237  tskurn  9240  pwinfi3  36212