Theorem tskuni 9161

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 9134	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ A e. T ) -> A ~< T )
2		cardidg 8923	. . . . . . . . . . . . . 14 |- ( T e. Tarski -> ( card ` T ) ~~ T )
3	2	ensymd 7566	. . . . . . . . . . . . 13 |- ( T e. Tarski -> T ~~ ( card ` T ) )
4	3	adantr 465	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ A e. T ) -> T ~~ ( card ` T ) )
5		sdomentr 7651	. . . . . . . . . . . 12 |- ( ( A ~< T /\ T ~~ ( card ` T ) ) -> A ~< ( card ` T ) )
6	1, 4, 5	syl2anc 661	. . . . . . . . . . 11 |- ( ( T e. Tarski /\ A e. T ) -> A ~< ( card ` T ) )
7		eqid 2467	. . . . . . . . . . . . . . 15 |- ( x e. A |-> ( f " x ) ) = ( x e. A |-> ( f " x ) )
8	7	rnmpt 5248	. . . . . . . . . . . . . 14 |- ran ( x e. A |-> ( f " x ) ) = { z | E. x e. A z = ( f " x ) }
9		cardon 8325	. . . . . . . . . . . . . . . . 17 |- ( card ` T ) e. On
10		sdomdom 7543	. . . . . . . . . . . . . . . . 17 |- ( A ~< ( card ` T ) -> A ~<_ ( card ` T ) )
11		ondomen 8418	. . . . . . . . . . . . . . . . 17 |- ( ( ( card ` T ) e. On /\ A ~<_ ( card ` T ) ) -> A e. dom card )
12	9, 10, 11	sylancr 663	. . . . . . . . . . . . . . . 16 |- ( A ~< ( card ` T ) -> A e. dom card )
13	12	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> A e. dom card )
14		vex 3116	. . . . . . . . . . . . . . . . . 18 |- f e. _V
15		imaexg 6721	. . . . . . . . . . . . . . . . . 18 |- ( f e. _V -> ( f " x ) e. _V )
16	14, 15	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( f " x ) e. _V
17	16, 7	fnmpti 5709	. . . . . . . . . . . . . . . 16 |- ( x e. A |-> ( f " x ) ) Fn A
18		dffn4 5801	. . . . . . . . . . . . . . . 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 8438	. . . . . . . . . . . . . . 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 4481	. . . . . . . . . . . . 13 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~<_ A )
23		domsdomtr 7652	. . . . . . . . . . . . 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 667	. . . . . . . . . . . 12 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
25	24	adantll 713	. . . . . . . . . . 11 |- ( ( ( T e. Tarski /\ A e. T ) /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
26	6, 25	mpdan 668	. . . . . . . . . 10 |- ( ( T e. Tarski /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
27		ne0i 3791	. . . . . . . . . . . 12 |- ( A e. T -> T =/= (/) )
28		tskcard 9159	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ T =/= (/) ) -> ( card ` T ) e. Inacc )
29	27, 28	sylan2 474	. . . . . . . . . . 11 |- ( ( T e. Tarski /\ A e. T ) -> ( card ` T ) e. Inacc )
30		elina 9065	. . . . . . . . . . . 12 |- ( ( card ` T ) e. Inacc <-> ( ( card ` T ) =/= (/) /\ ( cf ` ( card ` T ) ) = ( card ` T ) /\ A. x e. ( card ` T ) ~P x ~< ( card ` T ) ) )
31	30	simp2bi 1012	. . . . . . . . . . 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 4473	. . . . . . . . 9 |- ( ( T e. Tarski /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) )
34	33	3adant2 1015	. . . . . . . 8 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) )
35	34	adantr 465	. . . . . . 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 1015	. . . . . . . . . 10 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( card ` T ) e. Inacc )
37	36	adantr 465	. . . . . . . . 9 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> ( card ` T ) e. Inacc )
38		inawina 9068	. . . . . . . . 9 |- ( ( card ` T ) e. Inacc -> ( card ` T ) e. InaccW )
39		winalim 9073	. . . . . . . . 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 3116	. . . . . . . . . . 11 |- y e. _V
42		eqeq1 2471	. . . . . . . . . . . 12 |- ( z = y -> ( z = ( f " x ) <-> y = ( f " x ) ) )
43	42	rexbidv 2973	. . . . . . . . . . 11 |- ( z = y -> ( E. x e. A z = ( f " x ) <-> E. x e. A y = ( f " x ) ) )
44	41, 43	elab 3250	. . . . . . . . . 10 |- ( y e. { z | E. x e. A z = ( f " x ) } <-> E. x e. A y = ( f " x ) )
45		imassrn 5348	. . . . . . . . . . . . . 14 |- ( f " x ) C_ ran f
46		f1ofo 5823	. . . . . . . . . . . . . . 15 |- ( f : U. A -1-1-onto-> ( card ` T ) -> f : U. A -onto-> ( card ` T ) )
47		forn 5798	. . . . . . . . . . . . . . 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 3552	. . . . . . . . . . . . 13 |- ( f : U. A -1-1-onto-> ( card ` T ) -> ( f " x ) C_ ( card ` T ) )
50	49	ad2antlr 726	. . . . . . . . . . . 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 5815	. . . . . . . . . . . . . . . 16 |- ( f : U. A -1-1-onto-> ( card ` T ) -> f : U. A -1-1-> ( card ` T ) )
52		elssuni 4275	. . . . . . . . . . . . . . . 16 |- ( x e. A -> x C_ U. A )
53		vex 3116	. . . . . . . . . . . . . . . . 17 |- x e. _V
54	53	f1imaen 7577	. . . . . . . . . . . . . . . 16 |- ( ( f : U. A -1-1-> ( card ` T ) /\ x C_ U. A ) -> ( f " x ) ~~ x )
55	51, 52, 54	syl2an 477	. . . . . . . . . . . . . . 15 |- ( ( f : U. A -1-1-onto-> ( card ` T ) /\ x e. A ) -> ( f " x ) ~~ x )
56	55	adantll 713	. . . . . . . . . . . . . 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 999	. . . . . . . . . . . . . . . . 17 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> T e. Tarski )
58		trss 4549	. . . . . . . . . . . . . . . . . . . 20 |- ( Tr T -> ( A e. T -> A C_ T ) )
59	58	imp 429	. . . . . . . . . . . . . . . . . . 19 |- ( ( Tr T /\ A e. T ) -> A C_ T )
60	59	3adant1 1014	. . . . . . . . . . . . . . . . . 18 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> A C_ T )
61	60	sselda 3504	. . . . . . . . . . . . . . . . 17 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x e. T )
62		tsksdom 9134	. . . . . . . . . . . . . . . . 17 |- ( ( T e. Tarski /\ x e. T ) -> x ~< T )
63	57, 61, 62	syl2anc 661	. . . . . . . . . . . . . . . 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 7651	. . . . . . . . . . . . . . . 16 |- ( ( x ~< T /\ T ~~ ( card ` T ) ) -> x ~< ( card ` T ) )
66	63, 64, 65	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x ~< ( card ` T ) )
67	66	adantlr 714	. . . . . . . . . . . . . 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 7653	. . . . . . . . . . . . . 14 |- ( ( ( f " x ) ~~ x /\ x ~< ( card ` T ) ) -> ( f " x ) ~< ( card ` T ) )
69	56, 67, 68	syl2anc 661	. . . . . . . . . . . . 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 465	. . . . . . . . . . . . 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 4473	. . . . . . . . . . . 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 3525	. . . . . . . . . . . . . 14 |- ( y = ( f " x ) -> ( y C_ ( card ` T ) <-> ( f " x ) C_ ( card ` T ) ) )
74		breq1 4450	. . . . . . . . . . . . . 14 |- ( y = ( f " x ) -> ( y ~< ( cf ` ( card ` T ) ) <-> ( f " x ) ~< ( cf ` ( card ` T ) ) ) )
75	73, 74	anbi12d 710	. . . . . . . . . . . . 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 661	. . . . . . . . . . 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 2955	. . . . . . . . . 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 2876	. . . . . . . 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 5876	. . . . . . . . 9 |- ( card ` T ) e. _V
82	81	cfslb2n 8648	. . . . . . . 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 661	. . . . . . 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 4359	. . . . . . . 8 |- U_ x e. A ( f " x ) = U. { z | E. x e. A z = ( f " x ) }
86	49	ralrimivw 2879	. . . . . . . . . 10 |- ( f : U. A -1-1-onto-> ( card ` T ) -> A. x e. A ( f " x ) C_ ( card ` T ) )
87		iunss 4366	. . . . . . . . . 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 5795	. . . . . . . . . . . 12 |- ( f : U. A -onto-> ( card ` T ) -> f : U. A --> ( card ` T ) )
90		foelrn 6040	. . . . . . . . . . . . 13 |- ( ( f : U. A -onto-> ( card ` T ) /\ y e. ( card ` T ) ) -> E. z e. U. A y = ( f ` z ) )
91	90	ex 434	. . . . . . . . . . . 12 |- ( f : U. A -onto-> ( card ` T ) -> ( y e. ( card ` T ) -> E. z e. U. A y = ( f ` z ) ) )
92		eluni2 4249	. . . . . . . . . . . . . . 15 |- ( z e. U. A <-> E. x e. A z e. x )
93		nfv 1683	. . . . . . . . . . . . . . . 16 |- F/ x f : U. A --> ( card ` T )
94		nfiu1 4355	. . . . . . . . . . . . . . . . 17 |- F/_ x U_ x e. A ( f " x )
95	94	nfel2 2647	. . . . . . . . . . . . . . . 16 |- F/ x ( f ` z ) e. U_ x e. A ( f " x )
96		ssiun2 4368	. . . . . . . . . . . . . . . . . . 19 |- ( x e. A -> ( f " x ) C_ U_ x e. A ( f " x ) )
97	96	3ad2ant2 1018	. . . . . . . . . . . . . . . . . 18 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f " x ) C_ U_ x e. A ( f " x ) )
98		ffn 5731	. . . . . . . . . . . . . . . . . . . 20 |- ( f : U. A --> ( card ` T ) -> f Fn U. A )
99	98	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> f Fn U. A )
100	52	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> x C_ U. A )
101		simp3 998	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> z e. x )
102		fnfvima 6138	. . . . . . . . . . . . . . . . . . 19 |- ( ( f Fn U. A /\ x C_ U. A /\ z e. x ) -> ( f ` z ) e. ( f " x ) )
103	99, 100, 101, 102	syl3anc 1228	. . . . . . . . . . . . . . . . . 18 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f ` z ) e. ( f " x ) )
104	97, 103	sseldd 3505	. . . . . . . . . . . . . . . . 17 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f ` z ) e. U_ x e. A ( f " x ) )
105	104	3exp 1195	. . . . . . . . . . . . . . . 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 2947	. . . . . . . . . . . . . . 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 2550	. . . . . . . . . . . . . 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 2953	. . . . . . . . . . . 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 3510	. . . . . . . . 9 |- ( f : U. A -1-1-onto-> ( card ` T ) -> ( card ` T ) C_ U_ x e. A ( f " x ) )
114	88, 113	eqssd 3521	. . . . . . . 8 |- ( f : U. A -1-1-onto-> ( card ` T ) -> U_ x e. A ( f " x ) = ( card ` T ) )
115	85, 114	syl5eqr 2522	. . . . . . 7 |- ( f : U. A -1-1-onto-> ( card ` T ) -> U. { z | E. x e. A z = ( f " x ) } = ( card ` T ) )
116	115	necon3ai 2695	. . . . . 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 442	. . . 4 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. f : U. A -1-1-onto-> ( card ` T ) )
119	118	nexdv 1832	. . 3 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. E. f f : U. A -1-1-onto-> ( card ` T ) )
120		entr 7567	. . . . . . 7 |- ( ( U. A ~~ T /\ T ~~ ( card ` T ) ) -> U. A ~~ ( card ` T ) )
121	3, 120	sylan2 474	. . . . . 6 |- ( ( U. A ~~ T /\ T e. Tarski ) -> U. A ~~ ( card ` T ) )
122		bren 7525	. . . . . 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 435	. . . 4 |- ( T e. Tarski -> ( U. A ~~ T -> E. f f : U. A -1-1-onto-> ( card ` T ) ) )
125	124	3ad2ant1 1017	. . 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 4266	. . . . . . . . 9 |- ( A C_ T -> U. A C_ U. T )
128		df-tr 4541	. . . . . . . . . 10 |- ( Tr T <-> U. T C_ T )
129	128	biimpi 194	. . . . . . . . 9 |- ( Tr T -> U. T C_ T )
130	127, 129	sylan9ss 3517	. . . . . . . 8 |- ( ( A C_ T /\ Tr T ) -> U. A C_ T )
131	130	expcom 435	. . . . . . 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 429	. . . . 5 |- ( ( Tr T /\ A e. T ) -> U. A C_ T )
134		tsken 9132	. . . . 5 |- ( ( T e. Tarski /\ U. A C_ T ) -> ( U. A ~~ T \/ U. A e. T ) )
135	133, 134	sylan2 474	. . . 4 |- ( ( T e. Tarski /\ ( Tr T /\ A e. T ) ) -> ( U. A ~~ T \/ U. A e. T ) )
136	135	3impb 1192	. . 3 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( U. A ~~ T \/ U. A e. T ) )
137	136	ord 377	. 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 368   /\ wa 369   /\ w3a 973   = wceq 1379   E.wex 1596   e. wcel 1767   {cab 2452   =/= wne 2662   A.wral 2814   E.wrex 2815   _Vcvv 3113   C_ wss 3476   (/)c0 3785   ~Pcpw 4010   U.cuni 4245   U_ciun 4325   class class class wbr 4447   |-> cmpt 4505   Tr wtr 4540   Oncon0 4878   Lim wlim 4879   dom cdm 4999   ran crn 5000   "cima 5002   Fn wfn 5583   -->wf 5584   -1-1->wf1 5585   -onto->wfo 5586   -1-1-onto->wf1o 5587   ` cfv 5588   ~~ cen 7513   ~<_ cdom 7514   ~< csdm 7515   cardccrd 8316   cfccf 8318   InaccWcwina 9060   Inacccina 9061   Tarskictsk 9126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-inf2 8058  ax-ac2 8843

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-iin 4328  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-isom 5597  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-om 6685  df-1st 6784  df-2nd 6785  df-smo 7017  df-recs 7042  df-rdg 7076  df-1o 7130  df-2o 7131  df-oadd 7134  df-er 7311  df-map 7422  df-ixp 7470  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-oi 7935  df-har 7984  df-r1 8182  df-card 8320  df-aleph 8321  df-cf 8322  df-acn 8323  df-ac 8497  df-wina 9062  df-ina 9063  df-tsk 9127

This theorem is referenced by:  tskwun  9162  tskint  9163  tskun  9164  tskurn  9167