Theorem tskuni 8946

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 8919	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ A e. T ) -> A ~< T )
2		cardidg 8708	. . . . . . . . . . . . . 14 |- ( T e. Tarski -> ( card ` T ) ~~ T )
3	2	ensymd 7356	. . . . . . . . . . . . 13 |- ( T e. Tarski -> T ~~ ( card ` T ) )
4	3	adantr 462	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ A e. T ) -> T ~~ ( card ` T ) )
5		sdomentr 7441	. . . . . . . . . . . 12 |- ( ( A ~< T /\ T ~~ ( card ` T ) ) -> A ~< ( card ` T ) )
6	1, 4, 5	syl2anc 656	. . . . . . . . . . 11 |- ( ( T e. Tarski /\ A e. T ) -> A ~< ( card ` T ) )
7		eqid 2441	. . . . . . . . . . . . . . 15 |- ( x e. A |-> ( f " x ) ) = ( x e. A |-> ( f " x ) )
8	7	rnmpt 5081	. . . . . . . . . . . . . 14 |- ran ( x e. A |-> ( f " x ) ) = { z | E. x e. A z = ( f " x ) }
9		cardon 8110	. . . . . . . . . . . . . . . . 17 |- ( card ` T ) e. On
10		sdomdom 7333	. . . . . . . . . . . . . . . . 17 |- ( A ~< ( card ` T ) -> A ~<_ ( card ` T ) )
11		ondomen 8203	. . . . . . . . . . . . . . . . 17 |- ( ( ( card ` T ) e. On /\ A ~<_ ( card ` T ) ) -> A e. dom card )
12	9, 10, 11	sylancr 658	. . . . . . . . . . . . . . . 16 |- ( A ~< ( card ` T ) -> A e. dom card )
13	12	adantl 463	. . . . . . . . . . . . . . 15 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> A e. dom card )
14		vex 2973	. . . . . . . . . . . . . . . . . 18 |- f e. _V
15		imaexg 6514	. . . . . . . . . . . . . . . . . 18 |- ( f e. _V -> ( f " x ) e. _V )
16	14, 15	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( f " x ) e. _V
17	16, 7	fnmpti 5536	. . . . . . . . . . . . . . . 16 |- ( x e. A |-> ( f " x ) ) Fn A
18		dffn4 5623	. . . . . . . . . . . . . . . 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 8223	. . . . . . . . . . . . . . 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 4323	. . . . . . . . . . . . 13 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~<_ A )
23		domsdomtr 7442	. . . . . . . . . . . . 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 662	. . . . . . . . . . . 12 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
25	24	adantll 708	. . . . . . . . . . 11 |- ( ( ( T e. Tarski /\ A e. T ) /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
26	6, 25	mpdan 663	. . . . . . . . . 10 |- ( ( T e. Tarski /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
27		ne0i 3640	. . . . . . . . . . . 12 |- ( A e. T -> T =/= (/) )
28		tskcard 8944	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ T =/= (/) ) -> ( card ` T ) e. Inacc )
29	27, 28	sylan2 471	. . . . . . . . . . 11 |- ( ( T e. Tarski /\ A e. T ) -> ( card ` T ) e. Inacc )
30		elina 8850	. . . . . . . . . . . 12 |- ( ( card ` T ) e. Inacc <-> ( ( card ` T ) =/= (/) /\ ( cf ` ( card ` T ) ) = ( card ` T ) /\ A. x e. ( card ` T ) ~P x ~< ( card ` T ) ) )
31	30	simp2bi 999	. . . . . . . . . . 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 4315	. . . . . . . . 9 |- ( ( T e. Tarski /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) )
34	33	3adant2 1002	. . . . . . . 8 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) )
35	34	adantr 462	. . . . . . 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 1002	. . . . . . . . . 10 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( card ` T ) e. Inacc )
37	36	adantr 462	. . . . . . . . 9 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> ( card ` T ) e. Inacc )
38		inawina 8853	. . . . . . . . 9 |- ( ( card ` T ) e. Inacc -> ( card ` T ) e. InaccW )
39		winalim 8858	. . . . . . . . 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 2973	. . . . . . . . . . 11 |- y e. _V
42		eqeq1 2447	. . . . . . . . . . . 12 |- ( z = y -> ( z = ( f " x ) <-> y = ( f " x ) ) )
43	42	rexbidv 2734	. . . . . . . . . . 11 |- ( z = y -> ( E. x e. A z = ( f " x ) <-> E. x e. A y = ( f " x ) ) )
44	41, 43	elab 3103	. . . . . . . . . 10 |- ( y e. { z | E. x e. A z = ( f " x ) } <-> E. x e. A y = ( f " x ) )
45		imassrn 5177	. . . . . . . . . . . . . 14 |- ( f " x ) C_ ran f
46		f1ofo 5645	. . . . . . . . . . . . . . 15 |- ( f : U. A -1-1-onto-> ( card ` T ) -> f : U. A -onto-> ( card ` T ) )
47		forn 5620	. . . . . . . . . . . . . . 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 3401	. . . . . . . . . . . . 13 |- ( f : U. A -1-1-onto-> ( card ` T ) -> ( f " x ) C_ ( card ` T ) )
50	49	ad2antlr 721	. . . . . . . . . . . 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 5637	. . . . . . . . . . . . . . . 16 |- ( f : U. A -1-1-onto-> ( card ` T ) -> f : U. A -1-1-> ( card ` T ) )
52		elssuni 4118	. . . . . . . . . . . . . . . 16 |- ( x e. A -> x C_ U. A )
53		vex 2973	. . . . . . . . . . . . . . . . 17 |- x e. _V
54	53	f1imaen 7367	. . . . . . . . . . . . . . . 16 |- ( ( f : U. A -1-1-> ( card ` T ) /\ x C_ U. A ) -> ( f " x ) ~~ x )
55	51, 52, 54	syl2an 474	. . . . . . . . . . . . . . 15 |- ( ( f : U. A -1-1-onto-> ( card ` T ) /\ x e. A ) -> ( f " x ) ~~ x )
56	55	adantll 708	. . . . . . . . . . . . . 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 986	. . . . . . . . . . . . . . . . 17 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> T e. Tarski )
58		trss 4391	. . . . . . . . . . . . . . . . . . . 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 1001	. . . . . . . . . . . . . . . . . 18 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> A C_ T )
61	60	sselda 3353	. . . . . . . . . . . . . . . . 17 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x e. T )
62		tsksdom 8919	. . . . . . . . . . . . . . . . 17 |- ( ( T e. Tarski /\ x e. T ) -> x ~< T )
63	57, 61, 62	syl2anc 656	. . . . . . . . . . . . . . . 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 7441	. . . . . . . . . . . . . . . 16 |- ( ( x ~< T /\ T ~~ ( card ` T ) ) -> x ~< ( card ` T ) )
66	63, 64, 65	syl2anc 656	. . . . . . . . . . . . . . 15 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x ~< ( card ` T ) )
67	66	adantlr 709	. . . . . . . . . . . . . 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 7443	. . . . . . . . . . . . . 14 |- ( ( ( f " x ) ~~ x /\ x ~< ( card ` T ) ) -> ( f " x ) ~< ( card ` T ) )
69	56, 67, 68	syl2anc 656	. . . . . . . . . . . . 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 462	. . . . . . . . . . . . 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 4315	. . . . . . . . . . . 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 3374	. . . . . . . . . . . . . 14 |- ( y = ( f " x ) -> ( y C_ ( card ` T ) <-> ( f " x ) C_ ( card ` T ) ) )
74		breq1 4292	. . . . . . . . . . . . . 14 |- ( y = ( f " x ) -> ( y ~< ( cf ` ( card ` T ) ) <-> ( f " x ) ~< ( cf ` ( card ` T ) ) ) )
75	73, 74	anbi12d 705	. . . . . . . . . . . . 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 656	. . . . . . . . . . 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 2839	. . . . . . . . . 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 2796	. . . . . . . 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 5698	. . . . . . . . 9 |- ( card ` T ) e. _V
82	81	cfslb2n 8433	. . . . . . . 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 656	. . . . . . 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 4201	. . . . . . . 8 |- U_ x e. A ( f " x ) = U. { z | E. x e. A z = ( f " x ) }
86	49	ralrimivw 2798	. . . . . . . . . 10 |- ( f : U. A -1-1-onto-> ( card ` T ) -> A. x e. A ( f " x ) C_ ( card ` T ) )
87		iunss 4208	. . . . . . . . . 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 5617	. . . . . . . . . . . 12 |- ( f : U. A -onto-> ( card ` T ) -> f : U. A --> ( card ` T ) )
90		foelrn 5859	. . . . . . . . . . . . 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 4092	. . . . . . . . . . . . . . 15 |- ( z e. U. A <-> E. x e. A z e. x )
93		nfv 1678	. . . . . . . . . . . . . . . 16 |- F/ x f : U. A --> ( card ` T )
94		nfiu1 4197	. . . . . . . . . . . . . . . . 17 |- F/_ x U_ x e. A ( f " x )
95	94	nfel2 2589	. . . . . . . . . . . . . . . 16 |- F/ x ( f ` z ) e. U_ x e. A ( f " x )
96		ssiun2 4210	. . . . . . . . . . . . . . . . . . 19 |- ( x e. A -> ( f " x ) C_ U_ x e. A ( f " x ) )
97	96	3ad2ant2 1005	. . . . . . . . . . . . . . . . . 18 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f " x ) C_ U_ x e. A ( f " x ) )
98		ffn 5556	. . . . . . . . . . . . . . . . . . . 20 |- ( f : U. A --> ( card ` T ) -> f Fn U. A )
99	98	3ad2ant1 1004	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> f Fn U. A )
100	52	3ad2ant2 1005	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> x C_ U. A )
101		simp3 985	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> z e. x )
102		fnfvima 5952	. . . . . . . . . . . . . . . . . . 19 |- ( ( f Fn U. A /\ x C_ U. A /\ z e. x ) -> ( f ` z ) e. ( f " x ) )
103	99, 100, 101, 102	syl3anc 1213	. . . . . . . . . . . . . . . . . 18 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f ` z ) e. ( f " x ) )
104	97, 103	sseldd 3354	. . . . . . . . . . . . . . . . 17 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f ` z ) e. U_ x e. A ( f " x ) )
105	104	3exp 1181	. . . . . . . . . . . . . . . 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 2836	. . . . . . . . . . . . . . 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 2510	. . . . . . . . . . . . . 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 2838	. . . . . . . . . . . 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 3359	. . . . . . . . 9 |- ( f : U. A -1-1-onto-> ( card ` T ) -> ( card ` T ) C_ U_ x e. A ( f " x ) )
114	88, 113	eqssd 3370	. . . . . . . 8 |- ( f : U. A -1-1-onto-> ( card ` T ) -> U_ x e. A ( f " x ) = ( card ` T ) )
115	85, 114	syl5eqr 2487	. . . . . . 7 |- ( f : U. A -1-1-onto-> ( card ` T ) -> U. { z | E. x e. A z = ( f " x ) } = ( card ` T ) )
116	115	necon3ai 2649	. . . . . 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 1939	. . 3 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. E. f f : U. A -1-1-onto-> ( card ` T ) )
120		entr 7357	. . . . . . 7 |- ( ( U. A ~~ T /\ T ~~ ( card ` T ) ) -> U. A ~~ ( card ` T ) )
121	3, 120	sylan2 471	. . . . . 6 |- ( ( U. A ~~ T /\ T e. Tarski ) -> U. A ~~ ( card ` T ) )
122		bren 7315	. . . . . 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 1004	. . 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 4109	. . . . . . . . 9 |- ( A C_ T -> U. A C_ U. T )
128		df-tr 4383	. . . . . . . . . 10 |- ( Tr T <-> U. T C_ T )
129	128	biimpi 194	. . . . . . . . 9 |- ( Tr T -> U. T C_ T )
130	127, 129	sylan9ss 3366	. . . . . . . 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 8917	. . . . 5 |- ( ( T e. Tarski /\ U. A C_ T ) -> ( U. A ~~ T \/ U. A e. T ) )
135	133, 134	sylan2 471	. . . 4 |- ( ( T e. Tarski /\ ( Tr T /\ A e. T ) ) -> ( U. A ~~ T \/ U. A e. T ) )
136	135	3impb 1178	. . 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 960   = wceq 1364   E.wex 1591   e. wcel 1761   {cab 2427   =/= wne 2604   A.wral 2713   E.wrex 2714   _Vcvv 2970   C_ wss 3325   (/)c0 3634   ~Pcpw 3857   U.cuni 4088   U_ciun 4168   class class class wbr 4289   e. cmpt 4347   Tr wtr 4382   Oncon0 4715   Lim wlim 4716   dom cdm 4836   ran crn 4837   "cima 4839   Fn wfn 5410   -->wf 5411   -1-1->wf1 5412   -onto->wfo 5413   -1-1-onto->wf1o 5414   ` cfv 5415   ~~ cen 7303   ~<_ cdom 7304   ~< csdm 7305   cardccrd 8101   cfccf 8103   InaccWcwina 8845   Inacccina 8846   Tarskictsk 8911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-inf2 7843  ax-ac2 8628

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-iin 4171  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-se 4676  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-isom 5424  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-1st 6576  df-2nd 6577  df-smo 6803  df-recs 6828  df-rdg 6862  df-1o 6916  df-2o 6917  df-oadd 6920  df-er 7097  df-map 7212  df-ixp 7260  df-en 7307  df-dom 7308  df-sdom 7309  df-fin 7310  df-oi 7720  df-har 7769  df-r1 7967  df-card 8105  df-aleph 8106  df-cf 8107  df-acn 8108  df-ac 8282  df-wina 8847  df-ina 8848  df-tsk 8912

This theorem is referenced by:  tskwun  8947  tskint  8948  tskun  8949  tskurn  8952