This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

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