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 syl5bi ( ( ( 𝑇 ∈ 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 syl5bi ( 𝑓 : 𝐴 ⟶ ( 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 𝑇𝐴𝑇 ) → 𝐴𝑇 )