Theorem tskuni 9182

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

Proof of Theorem tskuni

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tsksdom 9155	. . . . . . . . . . . 12
2		cardidg 8944	. . . . . . . . . . . . . 14
3	2	ensymd 7586	. . . . . . . . . . . . 13
4	3	adantr 465	. . . . . . . . . . . 12
5		sdomentr 7671	. . . . . . . . . . . 12
6	1, 4, 5	syl2anc 661	. . . . . . . . . . 11
7		eqid 2457	. . . . . . . . . . . . . . 15
8	7	rnmpt 5253	. . . . . . . . . . . . . 14
9		cardon 8346	. . . . . . . . . . . . . . . . 17
10		sdomdom 7563	. . . . . . . . . . . . . . . . 17
11		ondomen 8439	. . . . . . . . . . . . . . . . 17
12	9, 10, 11	sylancr 663	. . . . . . . . . . . . . . . 16
13	12	adantl 466	. . . . . . . . . . . . . . 15
14		vex 3112	. . . . . . . . . . . . . . . . . 18
15		imaexg 6737	. . . . . . . . . . . . . . . . . 18
16	14, 15	ax-mp 5	. . . . . . . . . . . . . . . . 17
17	16, 7	fnmpti 5714	. . . . . . . . . . . . . . . 16
18		dffn4 5806	. . . . . . . . . . . . . . . 16
19	17, 18	mpbi 208	. . . . . . . . . . . . . . 15
20		fodomnum 8459	. . . . . . . . . . . . . . 15
21	13, 19, 20	mpisyl 18	. . . . . . . . . . . . . 14
22	8, 21	syl5eqbrr 4486	. . . . . . . . . . . . 13
23		domsdomtr 7672	. . . . . . . . . . . . 13
24	22, 23	sylancom 667	. . . . . . . . . . . 12
25	24	adantll 713	. . . . . . . . . . 11
26	6, 25	mpdan 668	. . . . . . . . . 10
27		ne0i 3790	. . . . . . . . . . . 12
28		tskcard 9180	. . . . . . . . . . . 12
29	27, 28	sylan2 474	. . . . . . . . . . 11
30		elina 9086	. . . . . . . . . . . 12
31	30	simp2bi 1012	. . . . . . . . . . 11
32	29, 31	syl 16	. . . . . . . . . 10
33	26, 32	breqtrrd 4478	. . . . . . . . 9
34	33	3adant2 1015	. . . . . . . 8
35	34	adantr 465	. . . . . . 7
36	29	3adant2 1015	. . . . . . . . . 10
37	36	adantr 465	. . . . . . . . 9
38		inawina 9089	. . . . . . . . 9
39		winalim 9094	. . . . . . . . 9
40	37, 38, 39	3syl 20	. . . . . . . 8
41		vex 3112	. . . . . . . . . . 11
42		eqeq1 2461	. . . . . . . . . . . 12
43	42	rexbidv 2968	. . . . . . . . . . 11
44	41, 43	elab 3246	. . . . . . . . . 10
45		imassrn 5353	. . . . . . . . . . . . . 14
46		f1ofo 5828	. . . . . . . . . . . . . . 15
47		forn 5803	. . . . . . . . . . . . . . 15
48	46, 47	syl 16	. . . . . . . . . . . . . 14
49	45, 48	syl5sseq 3551	. . . . . . . . . . . . 13
50	49	ad2antlr 726	. . . . . . . . . . . 12
51		f1of1 5820	. . . . . . . . . . . . . . . 16
52		elssuni 4279	. . . . . . . . . . . . . . . 16
53		vex 3112	. . . . . . . . . . . . . . . . 17
54	53	f1imaen 7597	. . . . . . . . . . . . . . . 16
55	51, 52, 54	syl2an 477	. . . . . . . . . . . . . . 15
56	55	adantll 713	. . . . . . . . . . . . . 14
57		simpl1 999	. . . . . . . . . . . . . . . . 17
58		trss 4554	. . . . . . . . . . . . . . . . . . . 20
59	58	imp 429	. . . . . . . . . . . . . . . . . . 19
60	59	3adant1 1014	. . . . . . . . . . . . . . . . . 18
61	60	sselda 3503	. . . . . . . . . . . . . . . . 17
62		tsksdom 9155	. . . . . . . . . . . . . . . . 17
63	57, 61, 62	syl2anc 661	. . . . . . . . . . . . . . . 16
64	57, 3	syl 16	. . . . . . . . . . . . . . . 16
65		sdomentr 7671	. . . . . . . . . . . . . . . 16
66	63, 64, 65	syl2anc 661	. . . . . . . . . . . . . . 15
67	66	adantlr 714	. . . . . . . . . . . . . 14
68		ensdomtr 7673	. . . . . . . . . . . . . 14
69	56, 67, 68	syl2anc 661	. . . . . . . . . . . . 13
70	37, 31	syl 16	. . . . . . . . . . . . . 14
71	70	adantr 465	. . . . . . . . . . . . 13
72	69, 71	breqtrrd 4478	. . . . . . . . . . . 12
73		sseq1 3524	. . . . . . . . . . . . . 14
74		breq1 4455	. . . . . . . . . . . . . 14
75	73, 74	anbi12d 710	. . . . . . . . . . . . 13
76	75	biimprcd 225	. . . . . . . . . . . 12
77	50, 72, 76	syl2anc 661	. . . . . . . . . . 11
78	77	rexlimdva 2949	. . . . . . . . . 10
79	44, 78	syl5bi 217	. . . . . . . . 9
80	79	ralrimiv 2869	. . . . . . . 8
81		fvex 5881	. . . . . . . . 9
82	81	cfslb2n 8669	. . . . . . . 8
83	40, 80, 82	syl2anc 661	. . . . . . 7
84	35, 83	mpd 15	. . . . . 6
85	16	dfiun2 4364	. . . . . . . 8
86	49	ralrimivw 2872	. . . . . . . . . 10
87		iunss 4371	. . . . . . . . . 10
88	86, 87	sylibr 212	. . . . . . . . 9
89		fof 5800	. . . . . . . . . . . 12
90		foelrn 6050	. . . . . . . . . . . . 13
91	90	ex 434	. . . . . . . . . . . 12
92		eluni2 4253	. . . . . . . . . . . . . . 15
93		nfv 1707	. . . . . . . . . . . . . . . 16
94		nfiu1 4360	. . . . . . . . . . . . . . . . 17
95	94	nfel2 2637	. . . . . . . . . . . . . . . 16
96		ssiun2 4373	. . . . . . . . . . . . . . . . . . 19
97	96	3ad2ant2 1018	. . . . . . . . . . . . . . . . . 18
98		ffn 5736	. . . . . . . . . . . . . . . . . . . 20
99	98	3ad2ant1 1017	. . . . . . . . . . . . . . . . . . 19
100	52	3ad2ant2 1018	. . . . . . . . . . . . . . . . . . 19
101		simp3 998	. . . . . . . . . . . . . . . . . . 19
102		fnfvima 6150	. . . . . . . . . . . . . . . . . . 19
103	99, 100, 101, 102	syl3anc 1228	. . . . . . . . . . . . . . . . . 18
104	97, 103	sseldd 3504	. . . . . . . . . . . . . . . . 17
105	104	3exp 1195	. . . . . . . . . . . . . . . 16
106	93, 95, 105	rexlimd 2941	. . . . . . . . . . . . . . 15
107	92, 106	syl5bi 217	. . . . . . . . . . . . . 14
108		eleq1a 2540	. . . . . . . . . . . . . 14
109	107, 108	syl6 33	. . . . . . . . . . . . 13
110	109	rexlimdv 2947	. . . . . . . . . . . 12
111	89, 91, 110	sylsyld 56	. . . . . . . . . . 11
112	46, 111	syl 16	. . . . . . . . . 10
113	112	ssrdv 3509	. . . . . . . . 9
114	88, 113	eqssd 3520	. . . . . . . 8
115	85, 114	syl5eqr 2512	. . . . . . 7
116	115	necon3ai 2685	. . . . . 6
117	84, 116	syl 16	. . . . 5
118	117	pm2.01da 442	. . . 4
119	118	nexdv 1884	. . 3
120		entr 7587	. . . . . . 7
121	3, 120	sylan2 474	. . . . . 6
122		bren 7545	. . . . . 6
123	121, 122	sylib 196	. . . . 5
124	123	expcom 435	. . . 4
125	124	3ad2ant1 1017	. . 3
126	119, 125	mtod 177	. 2
127		uniss 4270	. . . . . . . . 9
128		df-tr 4546	. . . . . . . . . 10
129	128	biimpi 194	. . . . . . . . 9
130	127, 129	sylan9ss 3516	. . . . . . . 8
131	130	expcom 435	. . . . . . 7
132	58, 131	syld 44	. . . . . 6
133	132	imp 429	. . . . 5
134		tsken 9153	. . . . 5
135	133, 134	sylan2 474	. . . 4
136	135	3impb 1192	. . 3
137	136	ord 377	. 2
138	126, 137	mpd 15	1

Syntax hints:  -.wn 3  ->wi 4  \/wo 368  /\wa 369  /\w3a 973  =wceq 1395  E.wex 1612  e.wcel 1818  {cab 2442  =/=wne 2652  A.wral 2807  E.wrex 2808  cvv 3109  C_wss 3475  c0 3784  ~Pcpw 4012  U.cuni 4249  U_ciun 4330   class class class wbr 4452  e.cmpt 4510  Trwtr 4545  con0 4883  Limwlim 4884  domcdm 5004  rancrn 5005  "cima 5007  Fnwfn 5588  -->wf 5589  -1-1->wf1 5590  -onto->wfo 5591  -1-1-onto->wf1o 5592  `cfv 5593  cen 7533  cdom 7534  csdm 7535  ccrd 8337  ccf 8339  cwina 9081  cina 9082  ctsk 9147

This theorem is referenced by:  tskwun  9183  tskint  9184  tskun  9185  tskurn  9188  pwinfi3  37748

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-inf2 8079  ax-ac2 8864

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-int 4287  df-iun 4332  df-iin 4333  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-se 4844  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-isom 5602  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-1st 6800  df-2nd 6801  df-smo 7036  df-recs 7061  df-rdg 7095  df-1o 7149  df-2o 7150  df-oadd 7153  df-er 7330  df-map 7441  df-ixp 7490  df-en 7537  df-dom 7538  df-sdom 7539  df-fin 7540  df-oi 7956  df-har 8005  df-r1 8203  df-card 8341  df-aleph 8342  df-cf 8343  df-acn 8344  df-ac 8518  df-wina 9083  df-ina 9084  df-tsk 9148