Theorem tskuni 9159

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 9132	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ A e. T ) -> A ~< T )
2		cardidg 8924	. . . . . . . . . . . . . 14 |- ( T e. Tarski -> ( card ` T ) ~~ T )
3	2	ensymd 7574	. . . . . . . . . . . . 13 |- ( T e. Tarski -> T ~~ ( card ` T ) )
4	3	adantr 466	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ A e. T ) -> T ~~ ( card ` T ) )
5		sdomentr 7659	. . . . . . . . . . . 12 |- ( ( A ~< T /\ T ~~ ( card ` T ) ) -> A ~< ( card ` T ) )
6	1, 4, 5	syl2anc 665	. . . . . . . . . . 11 |- ( ( T e. Tarski /\ A e. T ) -> A ~< ( card ` T ) )
7		eqid 2428	. . . . . . . . . . . . . . 15 |- ( x e. A |-> ( f " x ) ) = ( x e. A |-> ( f " x ) )
8	7	rnmpt 5042	. . . . . . . . . . . . . 14 |- ran ( x e. A |-> ( f " x ) ) = { z | E. x e. A z = ( f " x ) }
9		cardon 8330	. . . . . . . . . . . . . . . . 17 |- ( card ` T ) e. On
10		sdomdom 7551	. . . . . . . . . . . . . . . . 17 |- ( A ~< ( card ` T ) -> A ~<_ ( card ` T ) )
11		ondomen 8419	. . . . . . . . . . . . . . . . 17 |- ( ( ( card ` T ) e. On /\ A ~<_ ( card ` T ) ) -> A e. dom card )
12	9, 10, 11	sylancr 667	. . . . . . . . . . . . . . . 16 |- ( A ~< ( card ` T ) -> A e. dom card )
13	12	adantl 467	. . . . . . . . . . . . . . 15 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> A e. dom card )
14		vex 3025	. . . . . . . . . . . . . . . . . 18 |- f e. _V
15		imaexg 6688	. . . . . . . . . . . . . . . . . 18 |- ( f e. _V -> ( f " x ) e. _V )
16	14, 15	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( f " x ) e. _V
17	16, 7	fnmpti 5667	. . . . . . . . . . . . . . . 16 |- ( x e. A |-> ( f " x ) ) Fn A
18		dffn4 5759	. . . . . . . . . . . . . . . 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 211	. . . . . . . . . . . . . . 15 |- ( x e. A |-> ( f " x ) ) : A -onto-> ran ( x e. A |-> ( f " x ) )
20		fodomnum 8439	. . . . . . . . . . . . . . 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 4401	. . . . . . . . . . . . 13 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~<_ A )
23		domsdomtr 7660	. . . . . . . . . . . . 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 671	. . . . . . . . . . . 12 |- ( ( A e. T /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
25	24	adantll 718	. . . . . . . . . . 11 |- ( ( ( T e. Tarski /\ A e. T ) /\ A ~< ( card ` T ) ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
26	6, 25	mpdan 672	. . . . . . . . . 10 |- ( ( T e. Tarski /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( card ` T ) )
27		ne0i 3710	. . . . . . . . . . . 12 |- ( A e. T -> T =/= (/) )
28		tskcard 9157	. . . . . . . . . . . 12 |- ( ( T e. Tarski /\ T =/= (/) ) -> ( card ` T ) e. Inacc )
29	27, 28	sylan2 476	. . . . . . . . . . 11 |- ( ( T e. Tarski /\ A e. T ) -> ( card ` T ) e. Inacc )
30		elina 9063	. . . . . . . . . . . 12 |- ( ( card ` T ) e. Inacc <-> ( ( card ` T ) =/= (/) /\ ( cf ` ( card ` T ) ) = ( card ` T ) /\ A. x e. ( card ` T ) ~P x ~< ( card ` T ) ) )
31	30	simp2bi 1021	. . . . . . . . . . 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 4393	. . . . . . . . 9 |- ( ( T e. Tarski /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) )
34	33	3adant2 1024	. . . . . . . 8 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> { z | E. x e. A z = ( f " x ) } ~< ( cf ` ( card ` T ) ) )
35	34	adantr 466	. . . . . . 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 1024	. . . . . . . . . 10 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( card ` T ) e. Inacc )
37	36	adantr 466	. . . . . . . . 9 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ f : U. A -1-1-onto-> ( card ` T ) ) -> ( card ` T ) e. Inacc )
38		inawina 9066	. . . . . . . . 9 |- ( ( card ` T ) e. Inacc -> ( card ` T ) e. InaccW )
39		winalim 9071	. . . . . . . . 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 3025	. . . . . . . . . . 11 |- y e. _V
42		eqeq1 2432	. . . . . . . . . . . 12 |- ( z = y -> ( z = ( f " x ) <-> y = ( f " x ) ) )
43	42	rexbidv 2878	. . . . . . . . . . 11 |- ( z = y -> ( E. x e. A z = ( f " x ) <-> E. x e. A y = ( f " x ) ) )
44	41, 43	elab 3160	. . . . . . . . . 10 |- ( y e. { z | E. x e. A z = ( f " x ) } <-> E. x e. A y = ( f " x ) )
45		imassrn 5141	. . . . . . . . . . . . . 14 |- ( f " x ) C_ ran f
46		f1ofo 5781	. . . . . . . . . . . . . . 15 |- ( f : U. A -1-1-onto-> ( card ` T ) -> f : U. A -onto-> ( card ` T ) )
47		forn 5756	. . . . . . . . . . . . . . 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 3455	. . . . . . . . . . . . 13 |- ( f : U. A -1-1-onto-> ( card ` T ) -> ( f " x ) C_ ( card ` T ) )
50	49	ad2antlr 731	. . . . . . . . . . . 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 5773	. . . . . . . . . . . . . . . 16 |- ( f : U. A -1-1-onto-> ( card ` T ) -> f : U. A -1-1-> ( card ` T ) )
52		elssuni 4191	. . . . . . . . . . . . . . . 16 |- ( x e. A -> x C_ U. A )
53		vex 3025	. . . . . . . . . . . . . . . . 17 |- x e. _V
54	53	f1imaen 7585	. . . . . . . . . . . . . . . 16 |- ( ( f : U. A -1-1-> ( card ` T ) /\ x C_ U. A ) -> ( f " x ) ~~ x )
55	51, 52, 54	syl2an 479	. . . . . . . . . . . . . . 15 |- ( ( f : U. A -1-1-onto-> ( card ` T ) /\ x e. A ) -> ( f " x ) ~~ x )
56	55	adantll 718	. . . . . . . . . . . . . 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 1008	. . . . . . . . . . . . . . . . 17 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> T e. Tarski )
58		trss 4470	. . . . . . . . . . . . . . . . . . . 20 |- ( Tr T -> ( A e. T -> A C_ T ) )
59	58	imp 430	. . . . . . . . . . . . . . . . . . 19 |- ( ( Tr T /\ A e. T ) -> A C_ T )
60	59	3adant1 1023	. . . . . . . . . . . . . . . . . 18 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> A C_ T )
61	60	sselda 3407	. . . . . . . . . . . . . . . . 17 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x e. T )
62		tsksdom 9132	. . . . . . . . . . . . . . . . 17 |- ( ( T e. Tarski /\ x e. T ) -> x ~< T )
63	57, 61, 62	syl2anc 665	. . . . . . . . . . . . . . . 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 7659	. . . . . . . . . . . . . . . 16 |- ( ( x ~< T /\ T ~~ ( card ` T ) ) -> x ~< ( card ` T ) )
66	63, 64, 65	syl2anc 665	. . . . . . . . . . . . . . 15 |- ( ( ( T e. Tarski /\ Tr T /\ A e. T ) /\ x e. A ) -> x ~< ( card ` T ) )
67	66	adantlr 719	. . . . . . . . . . . . . 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 7661	. . . . . . . . . . . . . 14 |- ( ( ( f " x ) ~~ x /\ x ~< ( card ` T ) ) -> ( f " x ) ~< ( card ` T ) )
69	56, 67, 68	syl2anc 665	. . . . . . . . . . . . 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 466	. . . . . . . . . . . . 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 3428	. . . . . . . . . . . . . 14 |- ( y = ( f " x ) -> ( y C_ ( card ` T ) <-> ( f " x ) C_ ( card ` T ) ) )
74		breq1 4369	. . . . . . . . . . . . . 14 |- ( y = ( f " x ) -> ( y ~< ( cf ` ( card ` T ) ) <-> ( f " x ) ~< ( cf ` ( card ` T ) ) ) )
75	73, 74	anbi12d 715	. . . . . . . . . . . . 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 228	. . . . . . . . . . . 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 665	. . . . . . . . . . 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 2856	. . . . . . . . . 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 220	. . . . . . . . 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 2777	. . . . . . . 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 5835	. . . . . . . . 9 |- ( card ` T ) e. _V
82	81	cfslb2n 8649	. . . . . . . 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 665	. . . . . . 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 4276	. . . . . . . 8 |- U_ x e. A ( f " x ) = U. { z | E. x e. A z = ( f " x ) }
86	49	ralrimivw 2780	. . . . . . . . . 10 |- ( f : U. A -1-1-onto-> ( card ` T ) -> A. x e. A ( f " x ) C_ ( card ` T ) )
87		iunss 4283	. . . . . . . . . 10 |- ( U_ x e. A ( f " x ) C_ ( card ` T ) <-> A. x e. A ( f " x ) C_ ( card ` T ) )
88	86, 87	sylibr 215	. . . . . . . . 9 |- ( f : U. A -1-1-onto-> ( card ` T ) -> U_ x e. A ( f " x ) C_ ( card ` T ) )
89		fof 5753	. . . . . . . . . . . 12 |- ( f : U. A -onto-> ( card ` T ) -> f : U. A --> ( card ` T ) )
90		foelrn 6000	. . . . . . . . . . . . 13 |- ( ( f : U. A -onto-> ( card ` T ) /\ y e. ( card ` T ) ) -> E. z e. U. A y = ( f ` z ) )
91	90	ex 435	. . . . . . . . . . . 12 |- ( f : U. A -onto-> ( card ` T ) -> ( y e. ( card ` T ) -> E. z e. U. A y = ( f ` z ) ) )
92		eluni2 4166	. . . . . . . . . . . . . . 15 |- ( z e. U. A <-> E. x e. A z e. x )
93		nfv 1755	. . . . . . . . . . . . . . . 16 |- F/ x f : U. A --> ( card ` T )
94		nfiu1 4272	. . . . . . . . . . . . . . . . 17 |- F/_ x U_ x e. A ( f " x )
95	94	nfel2 2585	. . . . . . . . . . . . . . . 16 |- F/ x ( f ` z ) e. U_ x e. A ( f " x )
96		ssiun2 4285	. . . . . . . . . . . . . . . . . . 19 |- ( x e. A -> ( f " x ) C_ U_ x e. A ( f " x ) )
97	96	3ad2ant2 1027	. . . . . . . . . . . . . . . . . 18 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f " x ) C_ U_ x e. A ( f " x ) )
98		ffn 5689	. . . . . . . . . . . . . . . . . . . 20 |- ( f : U. A --> ( card ` T ) -> f Fn U. A )
99	98	3ad2ant1 1026	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> f Fn U. A )
100	52	3ad2ant2 1027	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> x C_ U. A )
101		simp3 1007	. . . . . . . . . . . . . . . . . . 19 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> z e. x )
102		fnfvima 6102	. . . . . . . . . . . . . . . . . . 19 |- ( ( f Fn U. A /\ x C_ U. A /\ z e. x ) -> ( f ` z ) e. ( f " x ) )
103	99, 100, 101, 102	syl3anc 1264	. . . . . . . . . . . . . . . . . 18 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f ` z ) e. ( f " x ) )
104	97, 103	sseldd 3408	. . . . . . . . . . . . . . . . 17 |- ( ( f : U. A --> ( card ` T ) /\ x e. A /\ z e. x ) -> ( f ` z ) e. U_ x e. A ( f " x ) )
105	104	3exp 1204	. . . . . . . . . . . . . . . 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 2848	. . . . . . . . . . . . . . 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 220	. . . . . . . . . . . . . 14 |- ( f : U. A --> ( card ` T ) -> ( z e. U. A -> ( f ` z ) e. U_ x e. A ( f " x ) ) )
108		eleq1a 2501	. . . . . . . . . . . . . 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 2854	. . . . . . . . . . . 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 3413	. . . . . . . . 9 |- ( f : U. A -1-1-onto-> ( card ` T ) -> ( card ` T ) C_ U_ x e. A ( f " x ) )
114	88, 113	eqssd 3424	. . . . . . . 8 |- ( f : U. A -1-1-onto-> ( card ` T ) -> U_ x e. A ( f " x ) = ( card ` T ) )
115	85, 114	syl5eqr 2476	. . . . . . 7 |- ( f : U. A -1-1-onto-> ( card ` T ) -> U. { z | E. x e. A z = ( f " x ) } = ( card ` T ) )
116	115	necon3ai 2626	. . . . . 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 443	. . . 4 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. f : U. A -1-1-onto-> ( card ` T ) )
119	118	nexdv 1775	. . 3 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. E. f f : U. A -1-1-onto-> ( card ` T ) )
120		entr 7575	. . . . . . 7 |- ( ( U. A ~~ T /\ T ~~ ( card ` T ) ) -> U. A ~~ ( card ` T ) )
121	3, 120	sylan2 476	. . . . . 6 |- ( ( U. A ~~ T /\ T e. Tarski ) -> U. A ~~ ( card ` T ) )
122		bren 7533	. . . . . 6 |- ( U. A ~~ ( card ` T ) <-> E. f f : U. A -1-1-onto-> ( card ` T ) )
123	121, 122	sylib 199	. . . . 5 |- ( ( U. A ~~ T /\ T e. Tarski ) -> E. f f : U. A -1-1-onto-> ( card ` T ) )
124	123	expcom 436	. . . 4 |- ( T e. Tarski -> ( U. A ~~ T -> E. f f : U. A -1-1-onto-> ( card ` T ) ) )
125	124	3ad2ant1 1026	. . 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 180	. 2 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> -. U. A ~~ T )
127		uniss 4183	. . . . . . . . 9 |- ( A C_ T -> U. A C_ U. T )
128		df-tr 4462	. . . . . . . . . 10 |- ( Tr T <-> U. T C_ T )
129	128	biimpi 197	. . . . . . . . 9 |- ( Tr T -> U. T C_ T )
130	127, 129	sylan9ss 3420	. . . . . . . 8 |- ( ( A C_ T /\ Tr T ) -> U. A C_ T )
131	130	expcom 436	. . . . . . 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 430	. . . . 5 |- ( ( Tr T /\ A e. T ) -> U. A C_ T )
134		tsken 9130	. . . . 5 |- ( ( T e. Tarski /\ U. A C_ T ) -> ( U. A ~~ T \/ U. A e. T ) )
135	133, 134	sylan2 476	. . . 4 |- ( ( T e. Tarski /\ ( Tr T /\ A e. T ) ) -> ( U. A ~~ T \/ U. A e. T ) )
136	135	3impb 1201	. . 3 |- ( ( T e. Tarski /\ Tr T /\ A e. T ) -> ( U. A ~~ T \/ U. A e. T ) )
137	136	ord 378	. 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 369   /\ wa 370   /\ w3a 982   = wceq 1437   E.wex 1657   e. wcel 1872   {cab 2414   =/= wne 2599   A.wral 2714   E.wrex 2715   _Vcvv 3022   C_ wss 3379   (/)c0 3704   ~Pcpw 3924   U.cuni 4162   U_ciun 4242   class class class wbr 4366   |-> cmpt 4425   Tr wtr 4461   dom cdm 4796   ran crn 4797   "cima 4799   Oncon0 5385   Lim wlim 5386   Fn wfn 5539   -->wf 5540   -1-1->wf1 5541   -onto->wfo 5542   -1-1-onto->wf1o 5543   ` cfv 5544   ~~ cen 7521   ~<_ cdom 7522   ~< csdm 7523   cardccrd 8321   cfccf 8323   InaccWcwina 9058   Inacccina 9059   Tarskictsk 9124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-inf2 8099  ax-ac2 8844

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-int 4199  df-iun 4244  df-iin 4245  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-se 4756  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-isom 5553  df-riota 6211  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-1st 6751  df-2nd 6752  df-wrecs 6983  df-smo 7020  df-recs 7045  df-rdg 7083  df-1o 7137  df-2o 7138  df-oadd 7141  df-er 7318  df-map 7429  df-ixp 7478  df-en 7525  df-dom 7526  df-sdom 7527  df-fin 7528  df-oi 7978  df-har 8026  df-r1 8187  df-card 8325  df-aleph 8326  df-cf 8327  df-acn 8328  df-ac 8498  df-wina 9060  df-ina 9061  df-tsk 9125

This theorem is referenced by:  tskwun  9160  tskint  9161  tskun  9162  tskurn  9165  pwinfi3  36080