tskuni

Description: The union of an element of a transitive Tarski class is in the set. (Contributed by Mario Carneiro, 22-Jun-2013)

		Ref	Expression
	Assertion	tskuni	$⊢ (T \in Tarski \land Tr T \land A \in T) \to ⋃ A \in T$

Proof

Step	Hyp	Ref	Expression
1		tsksdom	$⊢ (T \in Tarski \land A \in T) \to A ≺ T$
2		cardidg	$⊢ T \in Tarski \to card (T) \approx T$
3	2	ensymd	$⊢ T \in Tarski \to T \approx card (T)$
4	3	adantr	$⊢ (T \in Tarski \land A \in T) \to T \approx card (T)$
5		sdomentr	$⊢ (A ≺ T \land T \approx card (T)) \to A ≺ card (T)$
6	1 4 5	syl2anc	$⊢ (T \in Tarski \land A \in T) \to A ≺ card (T)$
7		eqid	$⊢ (x \in A ⟼ f [x]) = (x \in A ⟼ f [x])$
8	7	rnmpt	$⊢ ran (x \in A ⟼ f [x]) = \{z \| \exists x \in A z = f [x]\}$
9		cardon	$⊢ card (T) \in On$
10		sdomdom	$⊢ A ≺ card (T) \to A ≼ card (T)$
11		ondomen	$⊢ (card (T) \in On \land A ≼ card (T)) \to A \in dom card$
12	9 10 11	sylancr	$⊢ A ≺ card (T) \to A \in dom card$
13	12	adantl	$⊢ (A \in T \land A ≺ card (T)) \to A \in dom card$
14		vex	$⊢ f \in V$
15	14	imaex	$⊢ f [x] \in V$
16	15 7	fnmpti	$⊢ (x \in A ⟼ f [x]) Fn A$
17		dffn4	$⊢ (x \in A ⟼ f [x]) Fn A \leftrightarrow (x \in A ⟼ f [x]) : A \underset{onto}{⟶} ran (x \in A ⟼ f [x])$
18	16 17	mpbi	$⊢ (x \in A ⟼ f [x]) : A \underset{onto}{⟶} ran (x \in A ⟼ f [x])$
19		fodomnum	$⊢ A \in dom card \to ((x \in A ⟼ f [x]) : A \underset{onto}{⟶} ran (x \in A ⟼ f [x]) \to ran (x \in A ⟼ f [x]) ≼ A)$
20	13 18 19	mpisyl	$⊢ (A \in T \land A ≺ card (T)) \to ran (x \in A ⟼ f [x]) ≼ A$
21	8 20	eqbrtrrid	$⊢ (A \in T \land A ≺ card (T)) \to \{z \| \exists x \in A z = f [x]\} ≼ A$
22		domsdomtr	$⊢ (\{z \| \exists x \in A z = f [x]\} ≼ A \land A ≺ card (T)) \to \{z \| \exists x \in A z = f [x]\} ≺ card (T)$
23	21 22	sylancom	$⊢ (A \in T \land A ≺ card (T)) \to \{z \| \exists x \in A z = f [x]\} ≺ card (T)$
24	23	adantll	$⊢ ((T \in Tarski \land A \in T) \land A ≺ card (T)) \to \{z \| \exists x \in A z = f [x]\} ≺ card (T)$
25	6 24	mpdan	$⊢ (T \in Tarski \land A \in T) \to \{z \| \exists x \in A z = f [x]\} ≺ card (T)$
26		ne0i	$⊢ A \in T \to T \neq \emptyset$
27		tskcard	$⊢ (T \in Tarski \land T \neq \emptyset) \to card (T) \in Inacc$
28	26 27	sylan2	$⊢ (T \in Tarski \land A \in T) \to card (T) \in Inacc$
29		elina	$⊢ card (T) \in Inacc \leftrightarrow (card (T) \neq \emptyset \land cf (card (T)) = card (T) \land \forall x \in card (T) 𝒫 x ≺ card (T))$
30	29	simp2bi	$⊢ card (T) \in Inacc \to cf (card (T)) = card (T)$
31	28 30	syl	$⊢ (T \in Tarski \land A \in T) \to cf (card (T)) = card (T)$
32	25 31	breqtrrd	$⊢ (T \in Tarski \land A \in T) \to \{z \| \exists x \in A z = f [x]\} ≺ cf (card (T))$
33	32	3adant2	$⊢ (T \in Tarski \land Tr T \land A \in T) \to \{z \| \exists x \in A z = f [x]\} ≺ cf (card (T))$
34	33	adantr	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \to \{z \| \exists x \in A z = f [x]\} ≺ cf (card (T))$
35	28	3adant2	$⊢ (T \in Tarski \land Tr T \land A \in T) \to card (T) \in Inacc$
36	35	adantr	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \to card (T) \in Inacc$
37		inawina	$⊢ card (T) \in Inacc \to card (T) \in {Inacc}_{𝑤}$
38		winalim	$⊢ card (T) \in {Inacc}_{𝑤} \to Lim card (T)$
39	36 37 38	3syl	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \to Lim card (T)$
40		vex	$⊢ y \in V$
41		eqeq1	$⊢ z = y \to (z = f [x] \leftrightarrow y = f [x])$
42	41	rexbidv	$⊢ z = y \to (\exists x \in A z = f [x] \leftrightarrow \exists x \in A y = f [x])$
43	40 42	elab	$⊢ y \in \{z \| \exists x \in A z = f [x]\} \leftrightarrow \exists x \in A y = f [x]$
44		imassrn	$⊢ f [x] \subseteq ran f$
45		f1ofo	$⊢ f : ⋃ A \underset{1-1 onto}{⟶} card (T) \to f : ⋃ A \underset{onto}{⟶} card (T)$
46		forn	$⊢ f : ⋃ A \underset{onto}{⟶} card (T) \to ran f = card (T)$
47	45 46	syl	$⊢ f : ⋃ A \underset{1-1 onto}{⟶} card (T) \to ran f = card (T)$
48	44 47	sseqtrid	$⊢ f : ⋃ A \underset{1-1 onto}{⟶} card (T) \to f [x] \subseteq card (T)$
49	48	ad2antlr	$⊢ (((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \land x \in A) \to f [x] \subseteq card (T)$
50		f1of1	$⊢ f : ⋃ A \underset{1-1 onto}{⟶} card (T) \to f : ⋃ A \underset{1-1}{⟶} card (T)$
51		elssuni	$⊢ x \in A \to x \subseteq ⋃ A$
52		vex	$⊢ x \in V$
53	52	f1imaen	$⊢ (f : ⋃ A \underset{1-1}{⟶} card (T) \land x \subseteq ⋃ A) \to f [x] \approx x$
54	50 51 53	syl2an	$⊢ (f : ⋃ A \underset{1-1 onto}{⟶} card (T) \land x \in A) \to f [x] \approx x$
55	54	adantll	$⊢ (((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \land x \in A) \to f [x] \approx x$
56		simpl1	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land x \in A) \to T \in Tarski$
57		trss	$⊢ Tr T \to (A \in T \to A \subseteq T)$
58	57	imp	$⊢ (Tr T \land A \in T) \to A \subseteq T$
59	58	3adant1	$⊢ (T \in Tarski \land Tr T \land A \in T) \to A \subseteq T$
60	59	sselda	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land x \in A) \to x \in T$
61		tsksdom	$⊢ (T \in Tarski \land x \in T) \to x ≺ T$
62	56 60 61	syl2anc	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land x \in A) \to x ≺ T$
63	56 3	syl	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land x \in A) \to T \approx card (T)$
64		sdomentr	$⊢ (x ≺ T \land T \approx card (T)) \to x ≺ card (T)$
65	62 63 64	syl2anc	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land x \in A) \to x ≺ card (T)$
66	65	adantlr	$⊢ (((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \land x \in A) \to x ≺ card (T)$
67		ensdomtr	$⊢ (f [x] \approx x \land x ≺ card (T)) \to f [x] ≺ card (T)$
68	55 66 67	syl2anc	$⊢ (((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \land x \in A) \to f [x] ≺ card (T)$
69	36 30	syl	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \to cf (card (T)) = card (T)$
70	69	adantr	$⊢ (((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \land x \in A) \to cf (card (T)) = card (T)$
71	68 70	breqtrrd	$⊢ (((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \land x \in A) \to f [x] ≺ cf (card (T))$
72		sseq1	$⊢ y = f [x] \to (y \subseteq card (T) \leftrightarrow f [x] \subseteq card (T))$
73		breq1	$⊢ y = f [x] \to (y ≺ cf (card (T)) \leftrightarrow f [x] ≺ cf (card (T)))$
74	72 73	anbi12d	$⊢ y = f [x] \to ((y \subseteq card (T) \land y ≺ cf (card (T))) \leftrightarrow (f [x] \subseteq card (T) \land f [x] ≺ cf (card (T))))$
75	74	biimprcd	$⊢ (f [x] \subseteq card (T) \land f [x] ≺ cf (card (T))) \to (y = f [x] \to (y \subseteq card (T) \land y ≺ cf (card (T))))$
76	49 71 75	syl2anc	$⊢ (((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \land x \in A) \to (y = f [x] \to (y \subseteq card (T) \land y ≺ cf (card (T))))$
77	76	rexlimdva	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \to (\exists x \in A y = f [x] \to (y \subseteq card (T) \land y ≺ cf (card (T))))$
78	43 77	biimtrid	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \to (y \in \{z \| \exists x \in A z = f [x]\} \to (y \subseteq card (T) \land y ≺ cf (card (T))))$
79	78	ralrimiv	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \to \forall y \in \{z \| \exists x \in A z = f [x]\} (y \subseteq card (T) \land y ≺ cf (card (T)))$
80		fvex	$⊢ card (T) \in V$
81	80	cfslb2n	$⊢ (Lim card (T) \land \forall y \in \{z \| \exists x \in A z = f [x]\} (y \subseteq card (T) \land y ≺ cf (card (T)))) \to (\{z \| \exists x \in A z = f [x]\} ≺ cf (card (T)) \to ⋃ \{z \| \exists x \in A z = f [x]\} \neq card (T))$
82	39 79 81	syl2anc	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \to (\{z \| \exists x \in A z = f [x]\} ≺ cf (card (T)) \to ⋃ \{z \| \exists x \in A z = f [x]\} \neq card (T))$
83	34 82	mpd	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \to ⋃ \{z \| \exists x \in A z = f [x]\} \neq card (T)$
84	15	dfiun2	$⊢ ⋃_{x \in A} f [x] = ⋃ \{z \| \exists x \in A z = f [x]\}$
85	48	ralrimivw	$⊢ f : ⋃ A \underset{1-1 onto}{⟶} card (T) \to \forall x \in A f [x] \subseteq card (T)$
86		iunss	$⊢ ⋃_{x \in A} f [x] \subseteq card (T) \leftrightarrow \forall x \in A f [x] \subseteq card (T)$
87	85 86	sylibr	$⊢ f : ⋃ A \underset{1-1 onto}{⟶} card (T) \to ⋃_{x \in A} f [x] \subseteq card (T)$
88		fof	$⊢ f : ⋃ A \underset{onto}{⟶} card (T) \to f : ⋃ A ⟶ card (T)$
89		foelrn	$⊢ (f : ⋃ A \underset{onto}{⟶} card (T) \land y \in card (T)) \to \exists z \in ⋃ A y = f (z)$
90	89	ex	$⊢ f : ⋃ A \underset{onto}{⟶} card (T) \to (y \in card (T) \to \exists z \in ⋃ A y = f (z))$
91		eluni2	$⊢ z \in ⋃ A \leftrightarrow \exists x \in A z \in x$
92		nfv	$⊢ Ⅎ x f : ⋃ A ⟶ card (T)$
93		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} f [x]$
94	93	nfel2	$⊢ Ⅎ x f (z) \in ⋃_{x \in A} f [x]$
95		ssiun2	$⊢ x \in A \to f [x] \subseteq ⋃_{x \in A} f [x]$
96	95	3ad2ant2	$⊢ (f : ⋃ A ⟶ card (T) \land x \in A \land z \in x) \to f [x] \subseteq ⋃_{x \in A} f [x]$
97		ffn	$⊢ f : ⋃ A ⟶ card (T) \to f Fn ⋃ A$
98	97	3ad2ant1	$⊢ (f : ⋃ A ⟶ card (T) \land x \in A \land z \in x) \to f Fn ⋃ A$
99	51	3ad2ant2	$⊢ (f : ⋃ A ⟶ card (T) \land x \in A \land z \in x) \to x \subseteq ⋃ A$
100		simp3	$⊢ (f : ⋃ A ⟶ card (T) \land x \in A \land z \in x) \to z \in x$
101		fnfvima	$⊢ (f Fn ⋃ A \land x \subseteq ⋃ A \land z \in x) \to f (z) \in f [x]$
102	98 99 100 101	syl3anc	$⊢ (f : ⋃ A ⟶ card (T) \land x \in A \land z \in x) \to f (z) \in f [x]$
103	96 102	sseldd	$⊢ (f : ⋃ A ⟶ card (T) \land x \in A \land z \in x) \to f (z) \in ⋃_{x \in A} f [x]$
104	103	3exp	$⊢ f : ⋃ A ⟶ card (T) \to (x \in A \to (z \in x \to f (z) \in ⋃_{x \in A} f [x]))$
105	92 94 104	rexlimd	$⊢ f : ⋃ A ⟶ card (T) \to (\exists x \in A z \in x \to f (z) \in ⋃_{x \in A} f [x])$
106	91 105	biimtrid	$⊢ f : ⋃ A ⟶ card (T) \to (z \in ⋃ A \to f (z) \in ⋃_{x \in A} f [x])$
107		eleq1a	$⊢ f (z) \in ⋃_{x \in A} f [x] \to (y = f (z) \to y \in ⋃_{x \in A} f [x])$
108	106 107	syl6	$⊢ f : ⋃ A ⟶ card (T) \to (z \in ⋃ A \to (y = f (z) \to y \in ⋃_{x \in A} f [x]))$
109	108	rexlimdv	$⊢ f : ⋃ A ⟶ card (T) \to (\exists z \in ⋃ A y = f (z) \to y \in ⋃_{x \in A} f [x])$
110	88 90 109	sylsyld	$⊢ f : ⋃ A \underset{onto}{⟶} card (T) \to (y \in card (T) \to y \in ⋃_{x \in A} f [x])$
111	45 110	syl	$⊢ f : ⋃ A \underset{1-1 onto}{⟶} card (T) \to (y \in card (T) \to y \in ⋃_{x \in A} f [x])$
112	111	ssrdv	$⊢ f : ⋃ A \underset{1-1 onto}{⟶} card (T) \to card (T) \subseteq ⋃_{x \in A} f [x]$
113	87 112	eqssd	$⊢ f : ⋃ A \underset{1-1 onto}{⟶} card (T) \to ⋃_{x \in A} f [x] = card (T)$
114	84 113	eqtr3id	$⊢ f : ⋃ A \underset{1-1 onto}{⟶} card (T) \to ⋃ \{z \| \exists x \in A z = f [x]\} = card (T)$
115	114	necon3ai	$⊢ ⋃ \{z \| \exists x \in A z = f [x]\} \neq card (T) \to \neg f : ⋃ A \underset{1-1 onto}{⟶} card (T)$
116	83 115	syl	$⊢ ((T \in Tarski \land Tr T \land A \in T) \land f : ⋃ A \underset{1-1 onto}{⟶} card (T)) \to \neg f : ⋃ A \underset{1-1 onto}{⟶} card (T)$
117	116	pm2.01da	$⊢ (T \in Tarski \land Tr T \land A \in T) \to \neg f : ⋃ A \underset{1-1 onto}{⟶} card (T)$
118	117	nexdv	$⊢ (T \in Tarski \land Tr T \land A \in T) \to \neg \exists f f : ⋃ A \underset{1-1 onto}{⟶} card (T)$
119		entr	$⊢ (⋃ A \approx T \land T \approx card (T)) \to ⋃ A \approx card (T)$
120	3 119	sylan2	$⊢ (⋃ A \approx T \land T \in Tarski) \to ⋃ A \approx card (T)$
121		bren	$⊢ ⋃ A \approx card (T) \leftrightarrow \exists f f : ⋃ A \underset{1-1 onto}{⟶} card (T)$
122	120 121	sylib	$⊢ (⋃ A \approx T \land T \in Tarski) \to \exists f f : ⋃ A \underset{1-1 onto}{⟶} card (T)$
123	122	expcom	$⊢ T \in Tarski \to (⋃ A \approx T \to \exists f f : ⋃ A \underset{1-1 onto}{⟶} card (T))$
124	123	3ad2ant1	$⊢ (T \in Tarski \land Tr T \land A \in T) \to (⋃ A \approx T \to \exists f f : ⋃ A \underset{1-1 onto}{⟶} card (T))$
125	118 124	mtod	$⊢ (T \in Tarski \land Tr T \land A \in T) \to \neg ⋃ A \approx T$
126		uniss	$⊢ A \subseteq T \to ⋃ A \subseteq ⋃ T$
127		df-tr	$⊢ Tr T \leftrightarrow ⋃ T \subseteq T$
128	127	biimpi	$⊢ Tr T \to ⋃ T \subseteq T$
129	126 128	sylan9ss	$⊢ (A \subseteq T \land Tr T) \to ⋃ A \subseteq T$
130	129	expcom	$⊢ Tr T \to (A \subseteq T \to ⋃ A \subseteq T)$
131	57 130	syld	$⊢ Tr T \to (A \in T \to ⋃ A \subseteq T)$
132	131	imp	$⊢ (Tr T \land A \in T) \to ⋃ A \subseteq T$
133		tsken	$⊢ (T \in Tarski \land ⋃ A \subseteq T) \to (⋃ A \approx T \lor ⋃ A \in T)$
134	132 133	sylan2	$⊢ (T \in Tarski \land (Tr T \land A \in T)) \to (⋃ A \approx T \lor ⋃ A \in T)$
135	134	3impb	$⊢ (T \in Tarski \land Tr T \land A \in T) \to (⋃ A \approx T \lor ⋃ A \in T)$
136	135	ord	$⊢ (T \in Tarski \land Tr T \land A \in T) \to (\neg ⋃ A \approx T \to ⋃ A \in T)$
137	125 136	mpd	$⊢ (T \in Tarski \land Tr T \land A \in T) \to ⋃ A \in T$

Metamath Proof Explorer

Theorem tskuni

Proof