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

Theorem tskuni 9793
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 9766 . . . . . . . . . . . 12 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → 𝐴𝑇)
2 cardidg 9558 . . . . . . . . . . . . . 14 (𝑇 ∈ Tarski → (card‘𝑇) ≈ 𝑇)
32ensymd 8168 . . . . . . . . . . . . 13 (𝑇 ∈ Tarski → 𝑇 ≈ (card‘𝑇))
43adantr 472 . . . . . . . . . . . 12 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → 𝑇 ≈ (card‘𝑇))
5 sdomentr 8255 . . . . . . . . . . . 12 ((𝐴𝑇𝑇 ≈ (card‘𝑇)) → 𝐴 ≺ (card‘𝑇))
61, 4, 5syl2anc 696 . . . . . . . . . . 11 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → 𝐴 ≺ (card‘𝑇))
7 eqid 2756 . . . . . . . . . . . . . . 15 (𝑥𝐴 ↦ (𝑓𝑥)) = (𝑥𝐴 ↦ (𝑓𝑥))
87rnmpt 5522 . . . . . . . . . . . . . 14 ran (𝑥𝐴 ↦ (𝑓𝑥)) = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)}
9 cardon 8956 . . . . . . . . . . . . . . . . 17 (card‘𝑇) ∈ On
10 sdomdom 8145 . . . . . . . . . . . . . . . . 17 (𝐴 ≺ (card‘𝑇) → 𝐴 ≼ (card‘𝑇))
11 ondomen 9046 . . . . . . . . . . . . . . . . 17 (((card‘𝑇) ∈ On ∧ 𝐴 ≼ (card‘𝑇)) → 𝐴 ∈ dom card)
129, 10, 11sylancr 698 . . . . . . . . . . . . . . . 16 (𝐴 ≺ (card‘𝑇) → 𝐴 ∈ dom card)
1312adantl 473 . . . . . . . . . . . . . . 15 ((𝐴𝑇𝐴 ≺ (card‘𝑇)) → 𝐴 ∈ dom card)
14 vex 3339 . . . . . . . . . . . . . . . . . 18 𝑓 ∈ V
1514imaex 7265 . . . . . . . . . . . . . . . . 17 (𝑓𝑥) ∈ V
1615, 7fnmpti 6179 . . . . . . . . . . . . . . . 16 (𝑥𝐴 ↦ (𝑓𝑥)) Fn 𝐴
17 dffn4 6278 . . . . . . . . . . . . . . . 16 ((𝑥𝐴 ↦ (𝑓𝑥)) Fn 𝐴 ↔ (𝑥𝐴 ↦ (𝑓𝑥)):𝐴onto→ran (𝑥𝐴 ↦ (𝑓𝑥)))
1816, 17mpbi 220 . . . . . . . . . . . . . . 15 (𝑥𝐴 ↦ (𝑓𝑥)):𝐴onto→ran (𝑥𝐴 ↦ (𝑓𝑥))
19 fodomnum 9066 . . . . . . . . . . . . . . 15 (𝐴 ∈ dom card → ((𝑥𝐴 ↦ (𝑓𝑥)):𝐴onto→ran (𝑥𝐴 ↦ (𝑓𝑥)) → ran (𝑥𝐴 ↦ (𝑓𝑥)) ≼ 𝐴))
2013, 18, 19mpisyl 21 . . . . . . . . . . . . . 14 ((𝐴𝑇𝐴 ≺ (card‘𝑇)) → ran (𝑥𝐴 ↦ (𝑓𝑥)) ≼ 𝐴)
218, 20syl5eqbrr 4836 . . . . . . . . . . . . 13 ((𝐴𝑇𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≼ 𝐴)
22 domsdomtr 8256 . . . . . . . . . . . . 13 (({𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≼ 𝐴𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (card‘𝑇))
2321, 22sylancom 704 . . . . . . . . . . . 12 ((𝐴𝑇𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (card‘𝑇))
2423adantll 752 . . . . . . . . . . 11 (((𝑇 ∈ Tarski ∧ 𝐴𝑇) ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (card‘𝑇))
256, 24mpdan 705 . . . . . . . . . 10 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (card‘𝑇))
26 ne0i 4060 . . . . . . . . . . . 12 (𝐴𝑇𝑇 ≠ ∅)
27 tskcard 9791 . . . . . . . . . . . 12 ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → (card‘𝑇) ∈ Inacc)
2826, 27sylan2 492 . . . . . . . . . . 11 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → (card‘𝑇) ∈ Inacc)
29 elina 9697 . . . . . . . . . . . 12 ((card‘𝑇) ∈ Inacc ↔ ((card‘𝑇) ≠ ∅ ∧ (cf‘(card‘𝑇)) = (card‘𝑇) ∧ ∀𝑥 ∈ (card‘𝑇)𝒫 𝑥 ≺ (card‘𝑇)))
3029simp2bi 1141 . . . . . . . . . . 11 ((card‘𝑇) ∈ Inacc → (cf‘(card‘𝑇)) = (card‘𝑇))
3128, 30syl 17 . . . . . . . . . 10 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → (cf‘(card‘𝑇)) = (card‘𝑇))
3225, 31breqtrrd 4828 . . . . . . . . 9 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)))
33323adant2 1126 . . . . . . . 8 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)))
3433adantr 472 . . . . . . 7 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)))
35283adant2 1126 . . . . . . . . . 10 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → (card‘𝑇) ∈ Inacc)
3635adantr 472 . . . . . . . . 9 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → (card‘𝑇) ∈ Inacc)
37 inawina 9700 . . . . . . . . 9 ((card‘𝑇) ∈ Inacc → (card‘𝑇) ∈ Inaccw)
38 winalim 9705 . . . . . . . . 9 ((card‘𝑇) ∈ Inaccw → Lim (card‘𝑇))
3936, 37, 383syl 18 . . . . . . . 8 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → Lim (card‘𝑇))
40 vex 3339 . . . . . . . . . . 11 𝑦 ∈ V
41 eqeq1 2760 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 = (𝑓𝑥) ↔ 𝑦 = (𝑓𝑥)))
4241rexbidv 3186 . . . . . . . . . . 11 (𝑧 = 𝑦 → (∃𝑥𝐴 𝑧 = (𝑓𝑥) ↔ ∃𝑥𝐴 𝑦 = (𝑓𝑥)))
4340, 42elab 3486 . . . . . . . . . 10 (𝑦 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ↔ ∃𝑥𝐴 𝑦 = (𝑓𝑥))
44 imassrn 5631 . . . . . . . . . . . . . 14 (𝑓𝑥) ⊆ ran 𝑓
45 f1ofo 6301 . . . . . . . . . . . . . . 15 (𝑓: 𝐴1-1-onto→(card‘𝑇) → 𝑓: 𝐴onto→(card‘𝑇))
46 forn 6275 . . . . . . . . . . . . . . 15 (𝑓: 𝐴onto→(card‘𝑇) → ran 𝑓 = (card‘𝑇))
4745, 46syl 17 . . . . . . . . . . . . . 14 (𝑓: 𝐴1-1-onto→(card‘𝑇) → ran 𝑓 = (card‘𝑇))
4844, 47syl5sseq 3790 . . . . . . . . . . . . 13 (𝑓: 𝐴1-1-onto→(card‘𝑇) → (𝑓𝑥) ⊆ (card‘𝑇))
4948ad2antlr 765 . . . . . . . . . . . 12 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑓𝑥) ⊆ (card‘𝑇))
50 f1of1 6293 . . . . . . . . . . . . . . . 16 (𝑓: 𝐴1-1-onto→(card‘𝑇) → 𝑓: 𝐴1-1→(card‘𝑇))
51 elssuni 4615 . . . . . . . . . . . . . . . 16 (𝑥𝐴𝑥 𝐴)
52 vex 3339 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
5352f1imaen 8179 . . . . . . . . . . . . . . . 16 ((𝑓: 𝐴1-1→(card‘𝑇) ∧ 𝑥 𝐴) → (𝑓𝑥) ≈ 𝑥)
5450, 51, 53syl2an 495 . . . . . . . . . . . . . . 15 ((𝑓: 𝐴1-1-onto→(card‘𝑇) ∧ 𝑥𝐴) → (𝑓𝑥) ≈ 𝑥)
5554adantll 752 . . . . . . . . . . . . . 14 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑓𝑥) ≈ 𝑥)
56 simpl1 1228 . . . . . . . . . . . . . . . . 17 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑇 ∈ Tarski)
57 trss 4909 . . . . . . . . . . . . . . . . . . . 20 (Tr 𝑇 → (𝐴𝑇𝐴𝑇))
5857imp 444 . . . . . . . . . . . . . . . . . . 19 ((Tr 𝑇𝐴𝑇) → 𝐴𝑇)
59583adant1 1125 . . . . . . . . . . . . . . . . . 18 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → 𝐴𝑇)
6059sselda 3740 . . . . . . . . . . . . . . . . 17 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑥𝑇)
61 tsksdom 9766 . . . . . . . . . . . . . . . . 17 ((𝑇 ∈ Tarski ∧ 𝑥𝑇) → 𝑥𝑇)
6256, 60, 61syl2anc 696 . . . . . . . . . . . . . . . 16 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑥𝑇)
6356, 3syl 17 . . . . . . . . . . . . . . . 16 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑇 ≈ (card‘𝑇))
64 sdomentr 8255 . . . . . . . . . . . . . . . 16 ((𝑥𝑇𝑇 ≈ (card‘𝑇)) → 𝑥 ≺ (card‘𝑇))
6562, 63, 64syl2anc 696 . . . . . . . . . . . . . . 15 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑥 ≺ (card‘𝑇))
6665adantlr 753 . . . . . . . . . . . . . 14 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → 𝑥 ≺ (card‘𝑇))
67 ensdomtr 8257 . . . . . . . . . . . . . 14 (((𝑓𝑥) ≈ 𝑥𝑥 ≺ (card‘𝑇)) → (𝑓𝑥) ≺ (card‘𝑇))
6855, 66, 67syl2anc 696 . . . . . . . . . . . . 13 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑓𝑥) ≺ (card‘𝑇))
6936, 30syl 17 . . . . . . . . . . . . . 14 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → (cf‘(card‘𝑇)) = (card‘𝑇))
7069adantr 472 . . . . . . . . . . . . 13 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (cf‘(card‘𝑇)) = (card‘𝑇))
7168, 70breqtrrd 4828 . . . . . . . . . . . 12 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑓𝑥) ≺ (cf‘(card‘𝑇)))
72 sseq1 3763 . . . . . . . . . . . . . 14 (𝑦 = (𝑓𝑥) → (𝑦 ⊆ (card‘𝑇) ↔ (𝑓𝑥) ⊆ (card‘𝑇)))
73 breq1 4803 . . . . . . . . . . . . . 14 (𝑦 = (𝑓𝑥) → (𝑦 ≺ (cf‘(card‘𝑇)) ↔ (𝑓𝑥) ≺ (cf‘(card‘𝑇))))
7472, 73anbi12d 749 . . . . . . . . . . . . 13 (𝑦 = (𝑓𝑥) → ((𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))) ↔ ((𝑓𝑥) ⊆ (card‘𝑇) ∧ (𝑓𝑥) ≺ (cf‘(card‘𝑇)))))
7574biimprcd 240 . . . . . . . . . . . 12 (((𝑓𝑥) ⊆ (card‘𝑇) ∧ (𝑓𝑥) ≺ (cf‘(card‘𝑇))) → (𝑦 = (𝑓𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
7649, 71, 75syl2anc 696 . . . . . . . . . . 11 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑦 = (𝑓𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
7776rexlimdva 3165 . . . . . . . . . 10 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → (∃𝑥𝐴 𝑦 = (𝑓𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
7843, 77syl5bi 232 . . . . . . . . 9 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → (𝑦 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
7978ralrimiv 3099 . . . . . . . 8 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → ∀𝑦 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))))
80 fvex 6358 . . . . . . . . 9 (card‘𝑇) ∈ V
8180cfslb2n 9278 . . . . . . . 8 ((Lim (card‘𝑇) ∧ ∀𝑦 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))) → ({𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≠ (card‘𝑇)))
8239, 79, 81syl2anc 696 . . . . . . 7 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → ({𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≠ (card‘𝑇)))
8334, 82mpd 15 . . . . . 6 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≠ (card‘𝑇))
8415dfiun2 4702 . . . . . . . 8 𝑥𝐴 (𝑓𝑥) = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)}
8548ralrimivw 3101 . . . . . . . . . 10 (𝑓: 𝐴1-1-onto→(card‘𝑇) → ∀𝑥𝐴 (𝑓𝑥) ⊆ (card‘𝑇))
86 iunss 4709 . . . . . . . . . 10 ( 𝑥𝐴 (𝑓𝑥) ⊆ (card‘𝑇) ↔ ∀𝑥𝐴 (𝑓𝑥) ⊆ (card‘𝑇))
8785, 86sylibr 224 . . . . . . . . 9 (𝑓: 𝐴1-1-onto→(card‘𝑇) → 𝑥𝐴 (𝑓𝑥) ⊆ (card‘𝑇))
88 fof 6272 . . . . . . . . . . . 12 (𝑓: 𝐴onto→(card‘𝑇) → 𝑓: 𝐴⟶(card‘𝑇))
89 foelrn 6537 . . . . . . . . . . . . 13 ((𝑓: 𝐴onto→(card‘𝑇) ∧ 𝑦 ∈ (card‘𝑇)) → ∃𝑧 𝐴𝑦 = (𝑓𝑧))
9089ex 449 . . . . . . . . . . . 12 (𝑓: 𝐴onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → ∃𝑧 𝐴𝑦 = (𝑓𝑧)))
91 eluni2 4588 . . . . . . . . . . . . . . 15 (𝑧 𝐴 ↔ ∃𝑥𝐴 𝑧𝑥)
92 nfv 1988 . . . . . . . . . . . . . . . 16 𝑥 𝑓: 𝐴⟶(card‘𝑇)
93 nfiu1 4698 . . . . . . . . . . . . . . . . 17 𝑥 𝑥𝐴 (𝑓𝑥)
9493nfel2 2915 . . . . . . . . . . . . . . . 16 𝑥(𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥)
95 ssiun2 4711 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐴 → (𝑓𝑥) ⊆ 𝑥𝐴 (𝑓𝑥))
96953ad2ant2 1129 . . . . . . . . . . . . . . . . . 18 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → (𝑓𝑥) ⊆ 𝑥𝐴 (𝑓𝑥))
97 ffn 6202 . . . . . . . . . . . . . . . . . . . 20 (𝑓: 𝐴⟶(card‘𝑇) → 𝑓 Fn 𝐴)
98973ad2ant1 1128 . . . . . . . . . . . . . . . . . . 19 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → 𝑓 Fn 𝐴)
99513ad2ant2 1129 . . . . . . . . . . . . . . . . . . 19 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → 𝑥 𝐴)
100 simp3 1133 . . . . . . . . . . . . . . . . . . 19 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → 𝑧𝑥)
101 fnfvima 6655 . . . . . . . . . . . . . . . . . . 19 ((𝑓 Fn 𝐴𝑥 𝐴𝑧𝑥) → (𝑓𝑧) ∈ (𝑓𝑥))
10298, 99, 100, 101syl3anc 1477 . . . . . . . . . . . . . . . . . 18 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → (𝑓𝑧) ∈ (𝑓𝑥))
10396, 102sseldd 3741 . . . . . . . . . . . . . . . . 17 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → (𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥))
1041033exp 1113 . . . . . . . . . . . . . . . 16 (𝑓: 𝐴⟶(card‘𝑇) → (𝑥𝐴 → (𝑧𝑥 → (𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥))))
10592, 94, 104rexlimd 3160 . . . . . . . . . . . . . . 15 (𝑓: 𝐴⟶(card‘𝑇) → (∃𝑥𝐴 𝑧𝑥 → (𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥)))
10691, 105syl5bi 232 . . . . . . . . . . . . . 14 (𝑓: 𝐴⟶(card‘𝑇) → (𝑧 𝐴 → (𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥)))
107 eleq1a 2830 . . . . . . . . . . . . . 14 ((𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥) → (𝑦 = (𝑓𝑧) → 𝑦 𝑥𝐴 (𝑓𝑥)))
108106, 107syl6 35 . . . . . . . . . . . . 13 (𝑓: 𝐴⟶(card‘𝑇) → (𝑧 𝐴 → (𝑦 = (𝑓𝑧) → 𝑦 𝑥𝐴 (𝑓𝑥))))
109108rexlimdv 3164 . . . . . . . . . . . 12 (𝑓: 𝐴⟶(card‘𝑇) → (∃𝑧 𝐴𝑦 = (𝑓𝑧) → 𝑦 𝑥𝐴 (𝑓𝑥)))
11088, 90, 109sylsyld 61 . . . . . . . . . . 11 (𝑓: 𝐴onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → 𝑦 𝑥𝐴 (𝑓𝑥)))
11145, 110syl 17 . . . . . . . . . 10 (𝑓: 𝐴1-1-onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → 𝑦 𝑥𝐴 (𝑓𝑥)))
112111ssrdv 3746 . . . . . . . . 9 (𝑓: 𝐴1-1-onto→(card‘𝑇) → (card‘𝑇) ⊆ 𝑥𝐴 (𝑓𝑥))
11387, 112eqssd 3757 . . . . . . . 8 (𝑓: 𝐴1-1-onto→(card‘𝑇) → 𝑥𝐴 (𝑓𝑥) = (card‘𝑇))
11484, 113syl5eqr 2804 . . . . . . 7 (𝑓: 𝐴1-1-onto→(card‘𝑇) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} = (card‘𝑇))
115114necon3ai 2953 . . . . . 6 ( {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≠ (card‘𝑇) → ¬ 𝑓: 𝐴1-1-onto→(card‘𝑇))
11683, 115syl 17 . . . . 5 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → ¬ 𝑓: 𝐴1-1-onto→(card‘𝑇))
117116pm2.01da 457 . . . 4 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → ¬ 𝑓: 𝐴1-1-onto→(card‘𝑇))
118117nexdv 2009 . . 3 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → ¬ ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇))
119 entr 8169 . . . . . . 7 (( 𝐴𝑇𝑇 ≈ (card‘𝑇)) → 𝐴 ≈ (card‘𝑇))
1203, 119sylan2 492 . . . . . 6 (( 𝐴𝑇𝑇 ∈ Tarski) → 𝐴 ≈ (card‘𝑇))
121 bren 8126 . . . . . 6 ( 𝐴 ≈ (card‘𝑇) ↔ ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇))
122120, 121sylib 208 . . . . 5 (( 𝐴𝑇𝑇 ∈ Tarski) → ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇))
123122expcom 450 . . . 4 (𝑇 ∈ Tarski → ( 𝐴𝑇 → ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇)))
1241233ad2ant1 1128 . . 3 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → ( 𝐴𝑇 → ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇)))
125118, 124mtod 189 . 2 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → ¬ 𝐴𝑇)
126 uniss 4606 . . . . . . . . 9 (𝐴𝑇 𝐴 𝑇)
127 df-tr 4901 . . . . . . . . . 10 (Tr 𝑇 𝑇𝑇)
128127biimpi 206 . . . . . . . . 9 (Tr 𝑇 𝑇𝑇)
129126, 128sylan9ss 3753 . . . . . . . 8 ((𝐴𝑇 ∧ Tr 𝑇) → 𝐴𝑇)
130129expcom 450 . . . . . . 7 (Tr 𝑇 → (𝐴𝑇 𝐴𝑇))
13157, 130syld 47 . . . . . 6 (Tr 𝑇 → (𝐴𝑇 𝐴𝑇))
132131imp 444 . . . . 5 ((Tr 𝑇𝐴𝑇) → 𝐴𝑇)
133 tsken 9764 . . . . 5 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → ( 𝐴𝑇 𝐴𝑇))
134132, 133sylan2 492 . . . 4 ((𝑇 ∈ Tarski ∧ (Tr 𝑇𝐴𝑇)) → ( 𝐴𝑇 𝐴𝑇))
1351343impb 1108 . . 3 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → ( 𝐴𝑇 𝐴𝑇))
136135ord 391 . 2 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → (¬ 𝐴𝑇 𝐴𝑇))
137125, 136mpd 15 1 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → 𝐴𝑇)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382  wa 383  w3a 1072   = wceq 1628  wex 1849  wcel 2135  {cab 2742  wne 2928  wral 3046  wrex 3047  wss 3711  c0 4054  𝒫 cpw 4298   cuni 4584   ciun 4668   class class class wbr 4800  cmpt 4877  Tr wtr 4900  dom cdm 5262  ran crn 5263  cima 5265  Oncon0 5880  Lim wlim 5881   Fn wfn 6040  wf 6041  1-1wf1 6042  ontowfo 6043  1-1-ontowf1o 6044  cfv 6045  cen 8114  cdom 8115  csdm 8116  cardccrd 8947  cfccf 8949  Inaccwcwina 9692  Inacccina 9693  Tarskictsk 9758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-rep 4919  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-inf2 8707  ax-ac2 9473
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-int 4624  df-iun 4670  df-iin 4671  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-se 5222  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-isom 6054  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-1st 7329  df-2nd 7330  df-wrecs 7572  df-smo 7608  df-recs 7633  df-rdg 7671  df-1o 7725  df-2o 7726  df-oadd 7729  df-er 7907  df-map 8021  df-ixp 8071  df-en 8118  df-dom 8119  df-sdom 8120  df-fin 8121  df-oi 8576  df-har 8624  df-r1 8796  df-card 8951  df-aleph 8952  df-cf 8953  df-acn 8954  df-ac 9125  df-wina 9694  df-ina 9695  df-tsk 9759
This theorem is referenced by:  tskwun  9794  tskint  9795  tskun  9796  tskurn  9799  pwinfi3  38366
  Copyright terms: Public domain W3C validator