tskuni - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tskuni		Structured version Visualization version GIF version

Theorem tskuni 10905

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	⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ∪ 𝐴 ∈ 𝑇)

Proof of Theorem tskuni Dummy variables 𝑓 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tsksdom 10878	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → 𝐴 ≺ 𝑇)
2		cardidg 10669	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ Tarski → (card‘𝑇) ≈ 𝑇)
3	2	ensymd 9068	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ Tarski → 𝑇 ≈ (card‘𝑇))
4	3	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → 𝑇 ≈ (card‘𝑇))
5		sdomentr 9166	. . . . . . . . . . . 12 ⊢ ((𝐴 ≺ 𝑇 ∧ 𝑇 ≈ (card‘𝑇)) → 𝐴 ≺ (card‘𝑇))
6	1, 4, 5	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → 𝐴 ≺ (card‘𝑇))
7		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥))
8	7	rnmpt 5949	. . . . . . . . . . . . . 14 ⊢ ran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)}
9		cardon 10060	. . . . . . . . . . . . . . . . 17 ⊢ (card‘𝑇) ∈ On
10		sdomdom 9043	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ≺ (card‘𝑇) → 𝐴 ≼ (card‘𝑇))
11		ondomen 10153	. . . . . . . . . . . . . . . . 17 ⊢ (((card‘𝑇) ∈ On ∧ 𝐴 ≼ (card‘𝑇)) → 𝐴 ∈ dom card)
12	9, 10, 11	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ≺ (card‘𝑇) → 𝐴 ∈ dom card)
13	12	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ 𝑇 ∧ 𝐴 ≺ (card‘𝑇)) → 𝐴 ∈ dom card)
14		vex 3458	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑓 ∈ V
15	14	imaex 7958	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 “ 𝑥) ∈ V
16	15, 7	fnmpti 6710	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) Fn 𝐴
17		dffn4 6830	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)):𝐴⟶ontoran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)))
18	16, 17	mpbi 233	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)):𝐴⟶ontoran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥))
19		fodomnum 10173	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ dom card → ((𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)):𝐴⟶ontoran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) → ran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) ≼ 𝐴))
20	13, 18, 19	mpisyl 22	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ 𝑇 ∧ 𝐴 ≺ (card‘𝑇)) → ran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) ≼ 𝐴)
21	8, 20	eqbrtrrid 5145	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ 𝑇 ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≼ 𝐴)
22		domsdomtr 9167	. . . . . . . . . . . . 13 ⊢ (({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≼ 𝐴 ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (card‘𝑇))
23	21, 22	sylancom 600	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ 𝑇 ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (card‘𝑇))
24	23	adantll 727	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (card‘𝑇))
25	6, 24	mpdan 700	. . . . . . . . . 10 ⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (card‘𝑇))
26		ne0i 4290	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ 𝑇 → 𝑇 ≠ ∅)
27		tskcard 10903	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → (card‘𝑇) ∈ Inacc)
28	26, 27	sylan2 605	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → (card‘𝑇) ∈ Inacc)
29		elina 10809	. . . . . . . . . . . 12 ⊢ ((card‘𝑇) ∈ Inacc ↔ ((card‘𝑇) ≠ ∅ ∧ (cf‘(card‘𝑇)) = (card‘𝑇) ∧ ∀𝑥 ∈ (card‘𝑇)𝒫 𝑥 ≺ (card‘𝑇)))
30	29	simp2bi 1164	. . . . . . . . . . 11 ⊢ ((card‘𝑇) ∈ Inacc → (cf‘(card‘𝑇)) = (card‘𝑇))
31	28, 30	syl 18	. . . . . . . . . 10 ⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → (cf‘(card‘𝑇)) = (card‘𝑇))
32	25, 31	breqtrrd 5137	. . . . . . . . 9 ⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (cf‘(card‘𝑇)))
33	32	3adant2 1149	. . . . . . . 8 ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (cf‘(card‘𝑇)))
34	33	adantr 486	. . . . . . 7 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (cf‘(card‘𝑇)))
35	28	3adant2 1149	. . . . . . . . . 10 ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → (card‘𝑇) ∈ Inacc)
36	35	adantr 486	. . . . . . . . 9 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) → (card‘𝑇) ∈ Inacc)
37		inawina 10812	. . . . . . . . 9 ⊢ ((card‘𝑇) ∈ Inacc → (card‘𝑇) ∈ Inacc_w)
38		winalim 10817	. . . . . . . . 9 ⊢ ((card‘𝑇) ∈ Inacc_w → Lim (card‘𝑇))
39	36, 37, 38	3syl 19	. . . . . . . 8 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) → Lim (card‘𝑇))
40		vex 3458	. . . . . . . . . . 11 ⊢ 𝑦 ∈ V
41		eqeq1 2767	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → (𝑧 = (𝑓 “ 𝑥) ↔ 𝑦 = (𝑓 “ 𝑥)))
42	41	rexbidv 3190	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → (∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥) ↔ ∃𝑥 ∈ 𝐴 𝑦 = (𝑓 “ 𝑥)))
43	40, 42	elab 3636	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ↔ ∃𝑥 ∈ 𝐴 𝑦 = (𝑓 “ 𝑥))
44		imassrn 6214	. . . . . . . . . . . . . 14 ⊢ (𝑓 “ 𝑥) ⊆ ran 𝑓
45		f1ofo 6860	. . . . . . . . . . . . . . 15 ⊢ (𝑓:∪ 𝐴⟶1-1onto(card‘𝑇) → 𝑓:∪ 𝐴⟶onto(card‘𝑇))
46		forn 6827	. . . . . . . . . . . . . . 15 ⊢ (𝑓:∪ 𝐴⟶onto(card‘𝑇) → ran 𝑓 = (card‘𝑇))
47	45, 46	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑓:∪ 𝐴⟶1-1onto(card‘𝑇) → ran 𝑓 = (card‘𝑇))
48	44, 47	sseqtrid 3955	. . . . . . . . . . . . 13 ⊢ (𝑓:∪ 𝐴⟶1-1onto(card‘𝑇) → (𝑓 “ 𝑥) ⊆ (card‘𝑇))
49	48	ad2antlr 740	. . . . . . . . . . . 12 ⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ 𝑥) ⊆ (card‘𝑇))
50		f1of1 6851	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:∪ 𝐴⟶1-1onto(card‘𝑇) → 𝑓:∪ 𝐴⟶1-1(card‘𝑇))
51		elssuni 4902	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴)
52		vex 3458	. . . . . . . . . . . . . . . . 17 ⊢ 𝑥 ∈ V
53	52	f1imaen 9080	. . . . . . . . . . . . . . . 16 ⊢ ((𝑓:∪ 𝐴⟶1-1(card‘𝑇) ∧ 𝑥 ⊆ ∪ 𝐴) → (𝑓 “ 𝑥) ≈ 𝑥)
54	50, 51, 53	syl2an 608	. . . . . . . . . . . . . . 15 ⊢ ((𝑓:∪ 𝐴⟶1-1onto(card‘𝑇) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ 𝑥) ≈ 𝑥)
55	54	adantll 727	. . . . . . . . . . . . . 14 ⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ 𝑥) ≈ 𝑥)
56		simpl1 1210	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑇 ∈ Tarski)
57		trss 5226	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Tr 𝑇 → (𝐴 ∈ 𝑇 → 𝐴 ⊆ 𝑇))
58	57	imp 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → 𝐴 ⊆ 𝑇)
59	58	3adant1 1148	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → 𝐴 ⊆ 𝑇)
60	59	sselda 3913	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑇)
61		tsksdom 10878	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇) → 𝑥 ≺ 𝑇)
62	56, 60, 61	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ 𝑇)
63	56, 3	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑇 ≈ (card‘𝑇))
64		sdomentr 9166	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ≺ 𝑇 ∧ 𝑇 ≈ (card‘𝑇)) → 𝑥 ≺ (card‘𝑇))
65	62, 63, 64	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ (card‘𝑇))
66	65	adantlr 728	. . . . . . . . . . . . . 14 ⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ (card‘𝑇))
67		ensdomtr 9168	. . . . . . . . . . . . . 14 ⊢ (((𝑓 “ 𝑥) ≈ 𝑥 ∧ 𝑥 ≺ (card‘𝑇)) → (𝑓 “ 𝑥) ≺ (card‘𝑇))
68	55, 66, 67	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ 𝑥) ≺ (card‘𝑇))
69	36, 30	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) → (cf‘(card‘𝑇)) = (card‘𝑇))
70	69	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (cf‘(card‘𝑇)) = (card‘𝑇))
71	68, 70	breqtrrd 5137	. . . . . . . . . . . 12 ⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ 𝑥) ≺ (cf‘(card‘𝑇)))
72		sseq1 3938	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑓 “ 𝑥) → (𝑦 ⊆ (card‘𝑇) ↔ (𝑓 “ 𝑥) ⊆ (card‘𝑇)))
73		breq1 5109	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (𝑓 “ 𝑥) → (𝑦 ≺ (cf‘(card‘𝑇)) ↔ (𝑓 “ 𝑥) ≺ (cf‘(card‘𝑇))))
74	72, 73	anbi12d 644	. . . . . . . . . . . . 13 ⊢ (𝑦 = (𝑓 “ 𝑥) → ((𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))) ↔ ((𝑓 “ 𝑥) ⊆ (card‘𝑇) ∧ (𝑓 “ 𝑥) ≺ (cf‘(card‘𝑇)))))
75	74	biimprcd 253	. . . . . . . . . . . 12 ⊢ (((𝑓 “ 𝑥) ⊆ (card‘𝑇) ∧ (𝑓 “ 𝑥) ≺ (cf‘(card‘𝑇))) → (𝑦 = (𝑓 “ 𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
76	49, 71, 75	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝑓 “ 𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
77	76	rexlimdva 3167	. . . . . . . . . 10 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) → (∃𝑥 ∈ 𝐴 𝑦 = (𝑓 “ 𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
78	43, 77	biimtrid 245	. . . . . . . . 9 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) → (𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
79	78	ralrimiv 3157	. . . . . . . 8 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) → ∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))))
80		fvex 6927	. . . . . . . . 9 ⊢ (card‘𝑇) ∈ V
81	80	cfslb2n 10383	. . . . . . . 8 ⊢ ((Lim (card‘𝑇) ∧ ∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))) → ({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (cf‘(card‘𝑇)) → ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≠ (card‘𝑇)))
82	39, 79, 81	syl2anc 596	. . . . . . 7 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) → ({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (cf‘(card‘𝑇)) → ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≠ (card‘𝑇)))
83	34, 82	mpd 16	. . . . . 6 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) → ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≠ (card‘𝑇))
84	15	dfiun2 4993	. . . . . . . 8 ⊢ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥) = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)}
85	48	ralrimivw 3162	. . . . . . . . . 10 ⊢ (𝑓:∪ 𝐴⟶1-1onto(card‘𝑇) → ∀𝑥 ∈ 𝐴 (𝑓 “ 𝑥) ⊆ (card‘𝑇))
86		iunss 5006	. . . . . . . . . 10 ⊢ (∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥) ⊆ (card‘𝑇) ↔ ∀𝑥 ∈ 𝐴 (𝑓 “ 𝑥) ⊆ (card‘𝑇))
87	85, 86	sylibr 237	. . . . . . . . 9 ⊢ (𝑓:∪ 𝐴⟶1-1onto(card‘𝑇) → ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥) ⊆ (card‘𝑇))
88		fof 6824	. . . . . . . . . . . 12 ⊢ (𝑓:∪ 𝐴⟶onto(card‘𝑇) → 𝑓:∪ 𝐴⟶(card‘𝑇))
89		foelrn 7137	. . . . . . . . . . . . 13 ⊢ ((𝑓:∪ 𝐴⟶onto(card‘𝑇) ∧ 𝑦 ∈ (card‘𝑇)) → ∃𝑧 ∈ ∪ 𝐴𝑦 = (𝑓‘𝑧))
90	89	ex 418	. . . . . . . . . . . 12 ⊢ (𝑓:∪ 𝐴⟶onto(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → ∃𝑧 ∈ ∪ 𝐴𝑦 = (𝑓‘𝑧)))
91		eluni2 4874	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ∪ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝑥)
92		nfv 1949	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥 𝑓:∪ 𝐴⟶(card‘𝑇)
93		nfiu1 4989	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥)
94	93	nfel2 2944	. . . . . . . . . . . . . . . 16 ⊢ Ⅎ𝑥(𝑓‘𝑧) ∈ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥)
95		ssiun2 5009	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝐴 → (𝑓 “ 𝑥) ⊆ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥))
96	95	3ad2ant2 1152	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓:∪ 𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (𝑓 “ 𝑥) ⊆ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥))
97		ffn 6737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓:∪ 𝐴⟶(card‘𝑇) → 𝑓 Fn ∪ 𝐴)
98	97	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:∪ 𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → 𝑓 Fn ∪ 𝐴)
99	51	3ad2ant2 1152	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:∪ 𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → 𝑥 ⊆ ∪ 𝐴)
100		simp3 1156	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓:∪ 𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝑥)
101		fnfvima 7268	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 Fn ∪ 𝐴 ∧ 𝑥 ⊆ ∪ 𝐴 ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ (𝑓 “ 𝑥))
102	98, 99, 100, 101	syl3anc 1399	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑓:∪ 𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ (𝑓 “ 𝑥))
103	96, 102	sseldd 3914	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓:∪ 𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥))
104	103	3exp 1137	. . . . . . . . . . . . . . . 16 ⊢ (𝑓:∪ 𝐴⟶(card‘𝑇) → (𝑥 ∈ 𝐴 → (𝑧 ∈ 𝑥 → (𝑓‘𝑧) ∈ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥))))
105	92, 94, 104	rexlimd 3273	. . . . . . . . . . . . . . 15 ⊢ (𝑓:∪ 𝐴⟶(card‘𝑇) → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝑥 → (𝑓‘𝑧) ∈ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥)))
106	91, 105	biimtrid 245	. . . . . . . . . . . . . 14 ⊢ (𝑓:∪ 𝐴⟶(card‘𝑇) → (𝑧 ∈ ∪ 𝐴 → (𝑓‘𝑧) ∈ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥)))
107		eleq1a 2859	. . . . . . . . . . . . . 14 ⊢ ((𝑓‘𝑧) ∈ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥) → (𝑦 = (𝑓‘𝑧) → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥)))
108	106, 107	syl6 36	. . . . . . . . . . . . 13 ⊢ (𝑓:∪ 𝐴⟶(card‘𝑇) → (𝑧 ∈ ∪ 𝐴 → (𝑦 = (𝑓‘𝑧) → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥))))
109	108	rexlimdv 3165	. . . . . . . . . . . 12 ⊢ (𝑓:∪ 𝐴⟶(card‘𝑇) → (∃𝑧 ∈ ∪ 𝐴𝑦 = (𝑓‘𝑧) → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥)))
110	88, 90, 109	sylsyld 62	. . . . . . . . . . 11 ⊢ (𝑓:∪ 𝐴⟶onto(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥)))
111	45, 110	syl 18	. . . . . . . . . 10 ⊢ (𝑓:∪ 𝐴⟶1-1onto(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥)))
112	111	ssrdv 3919	. . . . . . . . 9 ⊢ (𝑓:∪ 𝐴⟶1-1onto(card‘𝑇) → (card‘𝑇) ⊆ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥))
113	87, 112	eqssd 3930	. . . . . . . 8 ⊢ (𝑓:∪ 𝐴⟶1-1onto(card‘𝑇) → ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥) = (card‘𝑇))
114	84, 113	eqtr3id 2812	. . . . . . 7 ⊢ (𝑓:∪ 𝐴⟶1-1onto(card‘𝑇) → ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} = (card‘𝑇))
115	114	necon3ai 2984	. . . . . 6 ⊢ (∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≠ (card‘𝑇) → ¬ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇))
116	83, 115	syl 18	. . . . 5 ⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)) → ¬ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇))
117	116	pm2.01da 811	. . . 4 ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ¬ 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇))
118	117	nexdv 1971	. . 3 ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ¬ ∃𝑓 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇))
119		entr 9069	. . . . . . 7 ⊢ ((∪ 𝐴 ≈ 𝑇 ∧ 𝑇 ≈ (card‘𝑇)) → ∪ 𝐴 ≈ (card‘𝑇))
120	3, 119	sylan2 605	. . . . . 6 ⊢ ((∪ 𝐴 ≈ 𝑇 ∧ 𝑇 ∈ Tarski) → ∪ 𝐴 ≈ (card‘𝑇))
121		bren 9019	. . . . . 6 ⊢ (∪ 𝐴 ≈ (card‘𝑇) ↔ ∃𝑓 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇))
122	120, 121	sylib 221	. . . . 5 ⊢ ((∪ 𝐴 ≈ 𝑇 ∧ 𝑇 ∈ Tarski) → ∃𝑓 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇))
123	122	expcom 419	. . . 4 ⊢ (𝑇 ∈ Tarski → (∪ 𝐴 ≈ 𝑇 → ∃𝑓 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)))
124	123	3ad2ant1 1151	. . 3 ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → (∪ 𝐴 ≈ 𝑇 → ∃𝑓 𝑓:∪ 𝐴⟶1-1onto(card‘𝑇)))
125	118, 124	mtod 201	. 2 ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ¬ ∪ 𝐴 ≈ 𝑇)
126		uniss 4878	. . . . . . . . 9 ⊢ (𝐴 ⊆ 𝑇 → ∪ 𝐴 ⊆ ∪ 𝑇)
127		df-tr 5217	. . . . . . . . . 10 ⊢ (Tr 𝑇 ↔ ∪ 𝑇 ⊆ 𝑇)
128	127	biimpi 219	. . . . . . . . 9 ⊢ (Tr 𝑇 → ∪ 𝑇 ⊆ 𝑇)
129	126, 128	sylan9ss 3926	. . . . . . . 8 ⊢ ((𝐴 ⊆ 𝑇 ∧ Tr 𝑇) → ∪ 𝐴 ⊆ 𝑇)
130	129	expcom 419	. . . . . . 7 ⊢ (Tr 𝑇 → (𝐴 ⊆ 𝑇 → ∪ 𝐴 ⊆ 𝑇))
131	57, 130	syld 48	. . . . . 6 ⊢ (Tr 𝑇 → (𝐴 ∈ 𝑇 → ∪ 𝐴 ⊆ 𝑇))
132	131	imp 412	. . . . 5 ⊢ ((Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ∪ 𝐴 ⊆ 𝑇)
133		tsken 10876	. . . . 5 ⊢ ((𝑇 ∈ Tarski ∧ ∪ 𝐴 ⊆ 𝑇) → (∪ 𝐴 ≈ 𝑇 ∨ ∪ 𝐴 ∈ 𝑇))
134	132, 133	sylan2 605	. . . 4 ⊢ ((𝑇 ∈ Tarski ∧ (Tr 𝑇 ∧ 𝐴 ∈ 𝑇)) → (∪ 𝐴 ≈ 𝑇 ∨ ∪ 𝐴 ∈ 𝑇))
135	134	3impb 1132	. . 3 ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → (∪ 𝐴 ≈ 𝑇 ∨ ∪ 𝐴 ∈ 𝑇))
136	135	ord 878	. 2 ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → (¬ ∪ 𝐴 ≈ 𝑇 → ∪ 𝐴 ∈ 𝑇))
137	125, 136	mpd 16	1 ⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ∪ 𝐴 ∈ 𝑇)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2147 {cab 2741 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 ⊆ wss 3900 ∅c0 4281 𝒫 cpw 4560 ∪ cuni 4870 ∪ ciun 4954 class class class wbr 5106 ↦ cmpt 5190 Tr wtr 5216 dom cdm 5656 ran crn 5657 “ cima 5659 Oncon0 6386 Lim wlim 6387 Fn wfn 6559 ⟶wf 6560 ⟶1-1wf1 6561 ⟶ontowfo 6562 ⟶1-1ontowf1o 6563 ‘cfv 6564 ≈ cen 9006 ≼ cdom 9007 ≺ csdm 9008 cardccrd 10051 cfccf 10053 Inacc_wcwina 10804 Inacccina 10805 Tarskictsk 10870

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7781 ax-inf2 9677 ax-ac2 10578

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6328 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6518 df-fun 6566 df-fn 6567 df-f 6568 df-f1 6569 df-fo 6570 df-f1o 6571 df-fv 6572 df-isom 6573 df-riota 7406 df-ov 7452 df-oprab 7453 df-mpo 7454 df-om 7910 df-1st 8033 df-2nd 8034 df-frecs 8335 df-wrecs 8366 df-smo 8390 df-recs 8415 df-rdg 8454 df-1o 8512 df-2o 8513 df-er 8753 df-map 8885 df-ixp 8962 df-en 9010 df-dom 9011 df-sdom 9012 df-fin 9013 df-oi 9539 df-har 9586 df-r1 9803 df-card 10055 df-aleph 10056 df-cf 10057 df-acn 10058 df-ac 10232 df-wina 10806 df-ina 10807 df-tsk 10871

This theorem is used by: tskwun 10906 tskint 10907 tskun 10908 tskurn 10911 pwinfi3 44819

W3C validator