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

Theorem tskuni 10194
 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.
StepHypRef Expression
1 tsksdom 10167 . . . . . . . . . . . 12 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → 𝐴𝑇)
2 cardidg 9959 . . . . . . . . . . . . . 14 (𝑇 ∈ Tarski → (card‘𝑇) ≈ 𝑇)
32ensymd 8543 . . . . . . . . . . . . 13 (𝑇 ∈ Tarski → 𝑇 ≈ (card‘𝑇))
43adantr 484 . . . . . . . . . . . 12 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → 𝑇 ≈ (card‘𝑇))
5 sdomentr 8635 . . . . . . . . . . . 12 ((𝐴𝑇𝑇 ≈ (card‘𝑇)) → 𝐴 ≺ (card‘𝑇))
61, 4, 5syl2anc 587 . . . . . . . . . . 11 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → 𝐴 ≺ (card‘𝑇))
7 eqid 2798 . . . . . . . . . . . . . . 15 (𝑥𝐴 ↦ (𝑓𝑥)) = (𝑥𝐴 ↦ (𝑓𝑥))
87rnmpt 5791 . . . . . . . . . . . . . 14 ran (𝑥𝐴 ↦ (𝑓𝑥)) = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)}
9 cardon 9357 . . . . . . . . . . . . . . . . 17 (card‘𝑇) ∈ On
10 sdomdom 8520 . . . . . . . . . . . . . . . . 17 (𝐴 ≺ (card‘𝑇) → 𝐴 ≼ (card‘𝑇))
11 ondomen 9448 . . . . . . . . . . . . . . . . 17 (((card‘𝑇) ∈ On ∧ 𝐴 ≼ (card‘𝑇)) → 𝐴 ∈ dom card)
129, 10, 11sylancr 590 . . . . . . . . . . . . . . . 16 (𝐴 ≺ (card‘𝑇) → 𝐴 ∈ dom card)
1312adantl 485 . . . . . . . . . . . . . . 15 ((𝐴𝑇𝐴 ≺ (card‘𝑇)) → 𝐴 ∈ dom card)
14 vex 3444 . . . . . . . . . . . . . . . . . 18 𝑓 ∈ V
1514imaex 7603 . . . . . . . . . . . . . . . . 17 (𝑓𝑥) ∈ V
1615, 7fnmpti 6463 . . . . . . . . . . . . . . . 16 (𝑥𝐴 ↦ (𝑓𝑥)) Fn 𝐴
17 dffn4 6571 . . . . . . . . . . . . . . . 16 ((𝑥𝐴 ↦ (𝑓𝑥)) Fn 𝐴 ↔ (𝑥𝐴 ↦ (𝑓𝑥)):𝐴onto→ran (𝑥𝐴 ↦ (𝑓𝑥)))
1816, 17mpbi 233 . . . . . . . . . . . . . . 15 (𝑥𝐴 ↦ (𝑓𝑥)):𝐴onto→ran (𝑥𝐴 ↦ (𝑓𝑥))
19 fodomnum 9468 . . . . . . . . . . . . . . 15 (𝐴 ∈ dom card → ((𝑥𝐴 ↦ (𝑓𝑥)):𝐴onto→ran (𝑥𝐴 ↦ (𝑓𝑥)) → ran (𝑥𝐴 ↦ (𝑓𝑥)) ≼ 𝐴))
2013, 18, 19mpisyl 21 . . . . . . . . . . . . . 14 ((𝐴𝑇𝐴 ≺ (card‘𝑇)) → ran (𝑥𝐴 ↦ (𝑓𝑥)) ≼ 𝐴)
218, 20eqbrtrrid 5066 . . . . . . . . . . . . 13 ((𝐴𝑇𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≼ 𝐴)
22 domsdomtr 8636 . . . . . . . . . . . . 13 (({𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≼ 𝐴𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (card‘𝑇))
2321, 22sylancom 591 . . . . . . . . . . . 12 ((𝐴𝑇𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (card‘𝑇))
2423adantll 713 . . . . . . . . . . 11 (((𝑇 ∈ Tarski ∧ 𝐴𝑇) ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (card‘𝑇))
256, 24mpdan 686 . . . . . . . . . 10 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (card‘𝑇))
26 ne0i 4250 . . . . . . . . . . . 12 (𝐴𝑇𝑇 ≠ ∅)
27 tskcard 10192 . . . . . . . . . . . 12 ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → (card‘𝑇) ∈ Inacc)
2826, 27sylan2 595 . . . . . . . . . . 11 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → (card‘𝑇) ∈ Inacc)
29 elina 10098 . . . . . . . . . . . 12 ((card‘𝑇) ∈ Inacc ↔ ((card‘𝑇) ≠ ∅ ∧ (cf‘(card‘𝑇)) = (card‘𝑇) ∧ ∀𝑥 ∈ (card‘𝑇)𝒫 𝑥 ≺ (card‘𝑇)))
3029simp2bi 1143 . . . . . . . . . . 11 ((card‘𝑇) ∈ Inacc → (cf‘(card‘𝑇)) = (card‘𝑇))
3128, 30syl 17 . . . . . . . . . 10 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → (cf‘(card‘𝑇)) = (card‘𝑇))
3225, 31breqtrrd 5058 . . . . . . . . 9 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)))
33323adant2 1128 . . . . . . . 8 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)))
3433adantr 484 . . . . . . 7 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)))
35283adant2 1128 . . . . . . . . . 10 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → (card‘𝑇) ∈ Inacc)
3635adantr 484 . . . . . . . . 9 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → (card‘𝑇) ∈ Inacc)
37 inawina 10101 . . . . . . . . 9 ((card‘𝑇) ∈ Inacc → (card‘𝑇) ∈ Inaccw)
38 winalim 10106 . . . . . . . . 9 ((card‘𝑇) ∈ Inaccw → Lim (card‘𝑇))
3936, 37, 383syl 18 . . . . . . . 8 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → Lim (card‘𝑇))
40 vex 3444 . . . . . . . . . . 11 𝑦 ∈ V
41 eqeq1 2802 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 = (𝑓𝑥) ↔ 𝑦 = (𝑓𝑥)))
4241rexbidv 3256 . . . . . . . . . . 11 (𝑧 = 𝑦 → (∃𝑥𝐴 𝑧 = (𝑓𝑥) ↔ ∃𝑥𝐴 𝑦 = (𝑓𝑥)))
4340, 42elab 3615 . . . . . . . . . 10 (𝑦 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ↔ ∃𝑥𝐴 𝑦 = (𝑓𝑥))
44 imassrn 5907 . . . . . . . . . . . . . 14 (𝑓𝑥) ⊆ ran 𝑓
45 f1ofo 6597 . . . . . . . . . . . . . . 15 (𝑓: 𝐴1-1-onto→(card‘𝑇) → 𝑓: 𝐴onto→(card‘𝑇))
46 forn 6568 . . . . . . . . . . . . . . 15 (𝑓: 𝐴onto→(card‘𝑇) → ran 𝑓 = (card‘𝑇))
4745, 46syl 17 . . . . . . . . . . . . . 14 (𝑓: 𝐴1-1-onto→(card‘𝑇) → ran 𝑓 = (card‘𝑇))
4844, 47sseqtrid 3967 . . . . . . . . . . . . 13 (𝑓: 𝐴1-1-onto→(card‘𝑇) → (𝑓𝑥) ⊆ (card‘𝑇))
4948ad2antlr 726 . . . . . . . . . . . 12 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑓𝑥) ⊆ (card‘𝑇))
50 f1of1 6589 . . . . . . . . . . . . . . . 16 (𝑓: 𝐴1-1-onto→(card‘𝑇) → 𝑓: 𝐴1-1→(card‘𝑇))
51 elssuni 4830 . . . . . . . . . . . . . . . 16 (𝑥𝐴𝑥 𝐴)
52 vex 3444 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
5352f1imaen 8554 . . . . . . . . . . . . . . . 16 ((𝑓: 𝐴1-1→(card‘𝑇) ∧ 𝑥 𝐴) → (𝑓𝑥) ≈ 𝑥)
5450, 51, 53syl2an 598 . . . . . . . . . . . . . . 15 ((𝑓: 𝐴1-1-onto→(card‘𝑇) ∧ 𝑥𝐴) → (𝑓𝑥) ≈ 𝑥)
5554adantll 713 . . . . . . . . . . . . . 14 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑓𝑥) ≈ 𝑥)
56 simpl1 1188 . . . . . . . . . . . . . . . . 17 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑇 ∈ Tarski)
57 trss 5145 . . . . . . . . . . . . . . . . . . . 20 (Tr 𝑇 → (𝐴𝑇𝐴𝑇))
5857imp 410 . . . . . . . . . . . . . . . . . . 19 ((Tr 𝑇𝐴𝑇) → 𝐴𝑇)
59583adant1 1127 . . . . . . . . . . . . . . . . . 18 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → 𝐴𝑇)
6059sselda 3915 . . . . . . . . . . . . . . . . 17 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑥𝑇)
61 tsksdom 10167 . . . . . . . . . . . . . . . . 17 ((𝑇 ∈ Tarski ∧ 𝑥𝑇) → 𝑥𝑇)
6256, 60, 61syl2anc 587 . . . . . . . . . . . . . . . 16 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑥𝑇)
6356, 3syl 17 . . . . . . . . . . . . . . . 16 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑇 ≈ (card‘𝑇))
64 sdomentr 8635 . . . . . . . . . . . . . . . 16 ((𝑥𝑇𝑇 ≈ (card‘𝑇)) → 𝑥 ≺ (card‘𝑇))
6562, 63, 64syl2anc 587 . . . . . . . . . . . . . . 15 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑥 ≺ (card‘𝑇))
6665adantlr 714 . . . . . . . . . . . . . 14 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → 𝑥 ≺ (card‘𝑇))
67 ensdomtr 8637 . . . . . . . . . . . . . 14 (((𝑓𝑥) ≈ 𝑥𝑥 ≺ (card‘𝑇)) → (𝑓𝑥) ≺ (card‘𝑇))
6855, 66, 67syl2anc 587 . . . . . . . . . . . . 13 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑓𝑥) ≺ (card‘𝑇))
6936, 30syl 17 . . . . . . . . . . . . . 14 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → (cf‘(card‘𝑇)) = (card‘𝑇))
7069adantr 484 . . . . . . . . . . . . 13 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (cf‘(card‘𝑇)) = (card‘𝑇))
7168, 70breqtrrd 5058 . . . . . . . . . . . 12 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑓𝑥) ≺ (cf‘(card‘𝑇)))
72 sseq1 3940 . . . . . . . . . . . . . 14 (𝑦 = (𝑓𝑥) → (𝑦 ⊆ (card‘𝑇) ↔ (𝑓𝑥) ⊆ (card‘𝑇)))
73 breq1 5033 . . . . . . . . . . . . . 14 (𝑦 = (𝑓𝑥) → (𝑦 ≺ (cf‘(card‘𝑇)) ↔ (𝑓𝑥) ≺ (cf‘(card‘𝑇))))
7472, 73anbi12d 633 . . . . . . . . . . . . 13 (𝑦 = (𝑓𝑥) → ((𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))) ↔ ((𝑓𝑥) ⊆ (card‘𝑇) ∧ (𝑓𝑥) ≺ (cf‘(card‘𝑇)))))
7574biimprcd 253 . . . . . . . . . . . 12 (((𝑓𝑥) ⊆ (card‘𝑇) ∧ (𝑓𝑥) ≺ (cf‘(card‘𝑇))) → (𝑦 = (𝑓𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
7649, 71, 75syl2anc 587 . . . . . . . . . . 11 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑦 = (𝑓𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
7776rexlimdva 3243 . . . . . . . . . 10 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → (∃𝑥𝐴 𝑦 = (𝑓𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
7843, 77syl5bi 245 . . . . . . . . 9 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → (𝑦 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
7978ralrimiv 3148 . . . . . . . 8 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → ∀𝑦 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))))
80 fvex 6658 . . . . . . . . 9 (card‘𝑇) ∈ V
8180cfslb2n 9679 . . . . . . . 8 ((Lim (card‘𝑇) ∧ ∀𝑦 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))) → ({𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≠ (card‘𝑇)))
8239, 79, 81syl2anc 587 . . . . . . 7 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → ({𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≠ (card‘𝑇)))
8334, 82mpd 15 . . . . . 6 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≠ (card‘𝑇))
8415dfiun2 4920 . . . . . . . 8 𝑥𝐴 (𝑓𝑥) = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)}
8548ralrimivw 3150 . . . . . . . . . 10 (𝑓: 𝐴1-1-onto→(card‘𝑇) → ∀𝑥𝐴 (𝑓𝑥) ⊆ (card‘𝑇))
86 iunss 4932 . . . . . . . . . 10 ( 𝑥𝐴 (𝑓𝑥) ⊆ (card‘𝑇) ↔ ∀𝑥𝐴 (𝑓𝑥) ⊆ (card‘𝑇))
8785, 86sylibr 237 . . . . . . . . 9 (𝑓: 𝐴1-1-onto→(card‘𝑇) → 𝑥𝐴 (𝑓𝑥) ⊆ (card‘𝑇))
88 fof 6565 . . . . . . . . . . . 12 (𝑓: 𝐴onto→(card‘𝑇) → 𝑓: 𝐴⟶(card‘𝑇))
89 foelrn 6849 . . . . . . . . . . . . 13 ((𝑓: 𝐴onto→(card‘𝑇) ∧ 𝑦 ∈ (card‘𝑇)) → ∃𝑧 𝐴𝑦 = (𝑓𝑧))
9089ex 416 . . . . . . . . . . . 12 (𝑓: 𝐴onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → ∃𝑧 𝐴𝑦 = (𝑓𝑧)))
91 eluni2 4804 . . . . . . . . . . . . . . 15 (𝑧 𝐴 ↔ ∃𝑥𝐴 𝑧𝑥)
92 nfv 1915 . . . . . . . . . . . . . . . 16 𝑥 𝑓: 𝐴⟶(card‘𝑇)
93 nfiu1 4915 . . . . . . . . . . . . . . . . 17 𝑥 𝑥𝐴 (𝑓𝑥)
9493nfel2 2973 . . . . . . . . . . . . . . . 16 𝑥(𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥)
95 ssiun2 4934 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐴 → (𝑓𝑥) ⊆ 𝑥𝐴 (𝑓𝑥))
96953ad2ant2 1131 . . . . . . . . . . . . . . . . . 18 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → (𝑓𝑥) ⊆ 𝑥𝐴 (𝑓𝑥))
97 ffn 6487 . . . . . . . . . . . . . . . . . . . 20 (𝑓: 𝐴⟶(card‘𝑇) → 𝑓 Fn 𝐴)
98973ad2ant1 1130 . . . . . . . . . . . . . . . . . . 19 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → 𝑓 Fn 𝐴)
99513ad2ant2 1131 . . . . . . . . . . . . . . . . . . 19 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → 𝑥 𝐴)
100 simp3 1135 . . . . . . . . . . . . . . . . . . 19 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → 𝑧𝑥)
101 fnfvima 6973 . . . . . . . . . . . . . . . . . . 19 ((𝑓 Fn 𝐴𝑥 𝐴𝑧𝑥) → (𝑓𝑧) ∈ (𝑓𝑥))
10298, 99, 100, 101syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → (𝑓𝑧) ∈ (𝑓𝑥))
10396, 102sseldd 3916 . . . . . . . . . . . . . . . . 17 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → (𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥))
1041033exp 1116 . . . . . . . . . . . . . . . 16 (𝑓: 𝐴⟶(card‘𝑇) → (𝑥𝐴 → (𝑧𝑥 → (𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥))))
10592, 94, 104rexlimd 3276 . . . . . . . . . . . . . . 15 (𝑓: 𝐴⟶(card‘𝑇) → (∃𝑥𝐴 𝑧𝑥 → (𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥)))
10691, 105syl5bi 245 . . . . . . . . . . . . . 14 (𝑓: 𝐴⟶(card‘𝑇) → (𝑧 𝐴 → (𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥)))
107 eleq1a 2885 . . . . . . . . . . . . . 14 ((𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥) → (𝑦 = (𝑓𝑧) → 𝑦 𝑥𝐴 (𝑓𝑥)))
108106, 107syl6 35 . . . . . . . . . . . . 13 (𝑓: 𝐴⟶(card‘𝑇) → (𝑧 𝐴 → (𝑦 = (𝑓𝑧) → 𝑦 𝑥𝐴 (𝑓𝑥))))
109108rexlimdv 3242 . . . . . . . . . . . 12 (𝑓: 𝐴⟶(card‘𝑇) → (∃𝑧 𝐴𝑦 = (𝑓𝑧) → 𝑦 𝑥𝐴 (𝑓𝑥)))
11088, 90, 109sylsyld 61 . . . . . . . . . . 11 (𝑓: 𝐴onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → 𝑦 𝑥𝐴 (𝑓𝑥)))
11145, 110syl 17 . . . . . . . . . 10 (𝑓: 𝐴1-1-onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → 𝑦 𝑥𝐴 (𝑓𝑥)))
112111ssrdv 3921 . . . . . . . . 9 (𝑓: 𝐴1-1-onto→(card‘𝑇) → (card‘𝑇) ⊆ 𝑥𝐴 (𝑓𝑥))
11387, 112eqssd 3932 . . . . . . . 8 (𝑓: 𝐴1-1-onto→(card‘𝑇) → 𝑥𝐴 (𝑓𝑥) = (card‘𝑇))
11484, 113syl5eqr 2847 . . . . . . 7 (𝑓: 𝐴1-1-onto→(card‘𝑇) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} = (card‘𝑇))
115114necon3ai 3012 . . . . . 6 ( {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≠ (card‘𝑇) → ¬ 𝑓: 𝐴1-1-onto→(card‘𝑇))
11683, 115syl 17 . . . . 5 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → ¬ 𝑓: 𝐴1-1-onto→(card‘𝑇))
117116pm2.01da 798 . . . 4 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → ¬ 𝑓: 𝐴1-1-onto→(card‘𝑇))
118117nexdv 1937 . . 3 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → ¬ ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇))
119 entr 8544 . . . . . . 7 (( 𝐴𝑇𝑇 ≈ (card‘𝑇)) → 𝐴 ≈ (card‘𝑇))
1203, 119sylan2 595 . . . . . 6 (( 𝐴𝑇𝑇 ∈ Tarski) → 𝐴 ≈ (card‘𝑇))
121 bren 8501 . . . . . 6 ( 𝐴 ≈ (card‘𝑇) ↔ ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇))
122120, 121sylib 221 . . . . 5 (( 𝐴𝑇𝑇 ∈ Tarski) → ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇))
123122expcom 417 . . . 4 (𝑇 ∈ Tarski → ( 𝐴𝑇 → ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇)))
1241233ad2ant1 1130 . . 3 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → ( 𝐴𝑇 → ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇)))
125118, 124mtod 201 . 2 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → ¬ 𝐴𝑇)
126 uniss 4808 . . . . . . . . 9 (𝐴𝑇 𝐴 𝑇)
127 df-tr 5137 . . . . . . . . . 10 (Tr 𝑇 𝑇𝑇)
128127biimpi 219 . . . . . . . . 9 (Tr 𝑇 𝑇𝑇)
129126, 128sylan9ss 3928 . . . . . . . 8 ((𝐴𝑇 ∧ Tr 𝑇) → 𝐴𝑇)
130129expcom 417 . . . . . . 7 (Tr 𝑇 → (𝐴𝑇 𝐴𝑇))
13157, 130syld 47 . . . . . 6 (Tr 𝑇 → (𝐴𝑇 𝐴𝑇))
132131imp 410 . . . . 5 ((Tr 𝑇𝐴𝑇) → 𝐴𝑇)
133 tsken 10165 . . . . 5 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → ( 𝐴𝑇 𝐴𝑇))
134132, 133sylan2 595 . . . 4 ((𝑇 ∈ Tarski ∧ (Tr 𝑇𝐴𝑇)) → ( 𝐴𝑇 𝐴𝑇))
1351343impb 1112 . . 3 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → ( 𝐴𝑇 𝐴𝑇))
136135ord 861 . 2 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → (¬ 𝐴𝑇 𝐴𝑇))
137125, 136mpd 15 1 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → 𝐴𝑇)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∨ wo 844   ∧ w3a 1084   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776   ≠ wne 2987  ∀wral 3106  ∃wrex 3107   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  ∪ cuni 4800  ∪ ciun 4881   class class class wbr 5030   ↦ cmpt 5110  Tr wtr 5136  dom cdm 5519  ran crn 5520   “ cima 5522  Oncon0 6159  Lim wlim 6160   Fn wfn 6319  ⟶wf 6320  –1-1→wf1 6321  –onto→wfo 6322  –1-1-onto→wf1o 6323  ‘cfv 6324   ≈ cen 8489   ≼ cdom 8490   ≺ csdm 8491  cardccrd 9348  cfccf 9350  Inaccwcwina 10093  Inacccina 10094  Tarskictsk 10159 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-inf2 9088  ax-ac2 9874 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-smo 7966  df-recs 7991  df-rdg 8029  df-1o 8085  df-2o 8086  df-oadd 8089  df-er 8272  df-map 8391  df-ixp 8445  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-oi 8958  df-har 9005  df-r1 9177  df-card 9352  df-aleph 9353  df-cf 9354  df-acn 9355  df-ac 9527  df-wina 10095  df-ina 10096  df-tsk 10160 This theorem is referenced by:  tskwun  10195  tskint  10196  tskun  10197  tskurn  10200  pwinfi3  40257
 Copyright terms: Public domain W3C validator