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

Theorem tskuni 9484
 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 9457 . . . . . . . . . . . 12 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → 𝐴𝑇)
2 cardidg 9249 . . . . . . . . . . . . . 14 (𝑇 ∈ Tarski → (card‘𝑇) ≈ 𝑇)
32ensymd 7893 . . . . . . . . . . . . 13 (𝑇 ∈ Tarski → 𝑇 ≈ (card‘𝑇))
43adantr 480 . . . . . . . . . . . 12 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → 𝑇 ≈ (card‘𝑇))
5 sdomentr 7979 . . . . . . . . . . . 12 ((𝐴𝑇𝑇 ≈ (card‘𝑇)) → 𝐴 ≺ (card‘𝑇))
61, 4, 5syl2anc 691 . . . . . . . . . . 11 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → 𝐴 ≺ (card‘𝑇))
7 eqid 2610 . . . . . . . . . . . . . . 15 (𝑥𝐴 ↦ (𝑓𝑥)) = (𝑥𝐴 ↦ (𝑓𝑥))
87rnmpt 5292 . . . . . . . . . . . . . 14 ran (𝑥𝐴 ↦ (𝑓𝑥)) = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)}
9 cardon 8653 . . . . . . . . . . . . . . . . 17 (card‘𝑇) ∈ On
10 sdomdom 7869 . . . . . . . . . . . . . . . . 17 (𝐴 ≺ (card‘𝑇) → 𝐴 ≼ (card‘𝑇))
11 ondomen 8743 . . . . . . . . . . . . . . . . 17 (((card‘𝑇) ∈ On ∧ 𝐴 ≼ (card‘𝑇)) → 𝐴 ∈ dom card)
129, 10, 11sylancr 694 . . . . . . . . . . . . . . . 16 (𝐴 ≺ (card‘𝑇) → 𝐴 ∈ dom card)
1312adantl 481 . . . . . . . . . . . . . . 15 ((𝐴𝑇𝐴 ≺ (card‘𝑇)) → 𝐴 ∈ dom card)
14 vex 3176 . . . . . . . . . . . . . . . . . 18 𝑓 ∈ V
1514imaex 6996 . . . . . . . . . . . . . . . . 17 (𝑓𝑥) ∈ V
1615, 7fnmpti 5935 . . . . . . . . . . . . . . . 16 (𝑥𝐴 ↦ (𝑓𝑥)) Fn 𝐴
17 dffn4 6034 . . . . . . . . . . . . . . . 16 ((𝑥𝐴 ↦ (𝑓𝑥)) Fn 𝐴 ↔ (𝑥𝐴 ↦ (𝑓𝑥)):𝐴onto→ran (𝑥𝐴 ↦ (𝑓𝑥)))
1816, 17mpbi 219 . . . . . . . . . . . . . . 15 (𝑥𝐴 ↦ (𝑓𝑥)):𝐴onto→ran (𝑥𝐴 ↦ (𝑓𝑥))
19 fodomnum 8763 . . . . . . . . . . . . . . 15 (𝐴 ∈ dom card → ((𝑥𝐴 ↦ (𝑓𝑥)):𝐴onto→ran (𝑥𝐴 ↦ (𝑓𝑥)) → ran (𝑥𝐴 ↦ (𝑓𝑥)) ≼ 𝐴))
2013, 18, 19mpisyl 21 . . . . . . . . . . . . . 14 ((𝐴𝑇𝐴 ≺ (card‘𝑇)) → ran (𝑥𝐴 ↦ (𝑓𝑥)) ≼ 𝐴)
218, 20syl5eqbrr 4619 . . . . . . . . . . . . 13 ((𝐴𝑇𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≼ 𝐴)
22 domsdomtr 7980 . . . . . . . . . . . . 13 (({𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≼ 𝐴𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (card‘𝑇))
2321, 22sylancom 698 . . . . . . . . . . . 12 ((𝐴𝑇𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (card‘𝑇))
2423adantll 746 . . . . . . . . . . 11 (((𝑇 ∈ Tarski ∧ 𝐴𝑇) ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (card‘𝑇))
256, 24mpdan 699 . . . . . . . . . 10 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (card‘𝑇))
26 ne0i 3880 . . . . . . . . . . . 12 (𝐴𝑇𝑇 ≠ ∅)
27 tskcard 9482 . . . . . . . . . . . 12 ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) → (card‘𝑇) ∈ Inacc)
2826, 27sylan2 490 . . . . . . . . . . 11 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → (card‘𝑇) ∈ Inacc)
29 elina 9388 . . . . . . . . . . . 12 ((card‘𝑇) ∈ Inacc ↔ ((card‘𝑇) ≠ ∅ ∧ (cf‘(card‘𝑇)) = (card‘𝑇) ∧ ∀𝑥 ∈ (card‘𝑇)𝒫 𝑥 ≺ (card‘𝑇)))
3029simp2bi 1070 . . . . . . . . . . 11 ((card‘𝑇) ∈ Inacc → (cf‘(card‘𝑇)) = (card‘𝑇))
3128, 30syl 17 . . . . . . . . . 10 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → (cf‘(card‘𝑇)) = (card‘𝑇))
3225, 31breqtrrd 4611 . . . . . . . . 9 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)))
33323adant2 1073 . . . . . . . 8 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)))
3433adantr 480 . . . . . . 7 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)))
35283adant2 1073 . . . . . . . . . 10 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → (card‘𝑇) ∈ Inacc)
3635adantr 480 . . . . . . . . 9 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → (card‘𝑇) ∈ Inacc)
37 inawina 9391 . . . . . . . . 9 ((card‘𝑇) ∈ Inacc → (card‘𝑇) ∈ Inaccw)
38 winalim 9396 . . . . . . . . 9 ((card‘𝑇) ∈ Inaccw → Lim (card‘𝑇))
3936, 37, 383syl 18 . . . . . . . 8 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → Lim (card‘𝑇))
40 vex 3176 . . . . . . . . . . 11 𝑦 ∈ V
41 eqeq1 2614 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 = (𝑓𝑥) ↔ 𝑦 = (𝑓𝑥)))
4241rexbidv 3034 . . . . . . . . . . 11 (𝑧 = 𝑦 → (∃𝑥𝐴 𝑧 = (𝑓𝑥) ↔ ∃𝑥𝐴 𝑦 = (𝑓𝑥)))
4340, 42elab 3319 . . . . . . . . . 10 (𝑦 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ↔ ∃𝑥𝐴 𝑦 = (𝑓𝑥))
44 imassrn 5396 . . . . . . . . . . . . . 14 (𝑓𝑥) ⊆ ran 𝑓
45 f1ofo 6057 . . . . . . . . . . . . . . 15 (𝑓: 𝐴1-1-onto→(card‘𝑇) → 𝑓: 𝐴onto→(card‘𝑇))
46 forn 6031 . . . . . . . . . . . . . . 15 (𝑓: 𝐴onto→(card‘𝑇) → ran 𝑓 = (card‘𝑇))
4745, 46syl 17 . . . . . . . . . . . . . 14 (𝑓: 𝐴1-1-onto→(card‘𝑇) → ran 𝑓 = (card‘𝑇))
4844, 47syl5sseq 3616 . . . . . . . . . . . . 13 (𝑓: 𝐴1-1-onto→(card‘𝑇) → (𝑓𝑥) ⊆ (card‘𝑇))
4948ad2antlr 759 . . . . . . . . . . . 12 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑓𝑥) ⊆ (card‘𝑇))
50 f1of1 6049 . . . . . . . . . . . . . . . 16 (𝑓: 𝐴1-1-onto→(card‘𝑇) → 𝑓: 𝐴1-1→(card‘𝑇))
51 elssuni 4403 . . . . . . . . . . . . . . . 16 (𝑥𝐴𝑥 𝐴)
52 vex 3176 . . . . . . . . . . . . . . . . 17 𝑥 ∈ V
5352f1imaen 7904 . . . . . . . . . . . . . . . 16 ((𝑓: 𝐴1-1→(card‘𝑇) ∧ 𝑥 𝐴) → (𝑓𝑥) ≈ 𝑥)
5450, 51, 53syl2an 493 . . . . . . . . . . . . . . 15 ((𝑓: 𝐴1-1-onto→(card‘𝑇) ∧ 𝑥𝐴) → (𝑓𝑥) ≈ 𝑥)
5554adantll 746 . . . . . . . . . . . . . 14 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑓𝑥) ≈ 𝑥)
56 simpl1 1057 . . . . . . . . . . . . . . . . 17 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑇 ∈ Tarski)
57 trss 4689 . . . . . . . . . . . . . . . . . . . 20 (Tr 𝑇 → (𝐴𝑇𝐴𝑇))
5857imp 444 . . . . . . . . . . . . . . . . . . 19 ((Tr 𝑇𝐴𝑇) → 𝐴𝑇)
59583adant1 1072 . . . . . . . . . . . . . . . . . 18 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → 𝐴𝑇)
6059sselda 3568 . . . . . . . . . . . . . . . . 17 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑥𝑇)
61 tsksdom 9457 . . . . . . . . . . . . . . . . 17 ((𝑇 ∈ Tarski ∧ 𝑥𝑇) → 𝑥𝑇)
6256, 60, 61syl2anc 691 . . . . . . . . . . . . . . . 16 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑥𝑇)
6356, 3syl 17 . . . . . . . . . . . . . . . 16 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑇 ≈ (card‘𝑇))
64 sdomentr 7979 . . . . . . . . . . . . . . . 16 ((𝑥𝑇𝑇 ≈ (card‘𝑇)) → 𝑥 ≺ (card‘𝑇))
6562, 63, 64syl2anc 691 . . . . . . . . . . . . . . 15 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑥𝐴) → 𝑥 ≺ (card‘𝑇))
6665adantlr 747 . . . . . . . . . . . . . 14 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → 𝑥 ≺ (card‘𝑇))
67 ensdomtr 7981 . . . . . . . . . . . . . 14 (((𝑓𝑥) ≈ 𝑥𝑥 ≺ (card‘𝑇)) → (𝑓𝑥) ≺ (card‘𝑇))
6855, 66, 67syl2anc 691 . . . . . . . . . . . . 13 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑓𝑥) ≺ (card‘𝑇))
6936, 30syl 17 . . . . . . . . . . . . . 14 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → (cf‘(card‘𝑇)) = (card‘𝑇))
7069adantr 480 . . . . . . . . . . . . 13 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (cf‘(card‘𝑇)) = (card‘𝑇))
7168, 70breqtrrd 4611 . . . . . . . . . . . 12 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑓𝑥) ≺ (cf‘(card‘𝑇)))
72 sseq1 3589 . . . . . . . . . . . . . 14 (𝑦 = (𝑓𝑥) → (𝑦 ⊆ (card‘𝑇) ↔ (𝑓𝑥) ⊆ (card‘𝑇)))
73 breq1 4586 . . . . . . . . . . . . . 14 (𝑦 = (𝑓𝑥) → (𝑦 ≺ (cf‘(card‘𝑇)) ↔ (𝑓𝑥) ≺ (cf‘(card‘𝑇))))
7472, 73anbi12d 743 . . . . . . . . . . . . 13 (𝑦 = (𝑓𝑥) → ((𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))) ↔ ((𝑓𝑥) ⊆ (card‘𝑇) ∧ (𝑓𝑥) ≺ (cf‘(card‘𝑇)))))
7574biimprcd 239 . . . . . . . . . . . 12 (((𝑓𝑥) ⊆ (card‘𝑇) ∧ (𝑓𝑥) ≺ (cf‘(card‘𝑇))) → (𝑦 = (𝑓𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
7649, 71, 75syl2anc 691 . . . . . . . . . . 11 ((((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) ∧ 𝑥𝐴) → (𝑦 = (𝑓𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
7776rexlimdva 3013 . . . . . . . . . 10 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → (∃𝑥𝐴 𝑦 = (𝑓𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
7843, 77syl5bi 231 . . . . . . . . 9 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → (𝑦 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))))
7978ralrimiv 2948 . . . . . . . 8 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → ∀𝑦 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))))
80 fvex 6113 . . . . . . . . 9 (card‘𝑇) ∈ V
8180cfslb2n 8973 . . . . . . . 8 ((Lim (card‘𝑇) ∧ ∀𝑦 ∈ {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))) → ({𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≠ (card‘𝑇)))
8239, 79, 81syl2anc 691 . . . . . . 7 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → ({𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≺ (cf‘(card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≠ (card‘𝑇)))
8334, 82mpd 15 . . . . . 6 (((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) ∧ 𝑓: 𝐴1-1-onto→(card‘𝑇)) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} ≠ (card‘𝑇))
8415dfiun2 4490 . . . . . . . 8 𝑥𝐴 (𝑓𝑥) = {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)}
8548ralrimivw 2950 . . . . . . . . . 10 (𝑓: 𝐴1-1-onto→(card‘𝑇) → ∀𝑥𝐴 (𝑓𝑥) ⊆ (card‘𝑇))
86 iunss 4497 . . . . . . . . . 10 ( 𝑥𝐴 (𝑓𝑥) ⊆ (card‘𝑇) ↔ ∀𝑥𝐴 (𝑓𝑥) ⊆ (card‘𝑇))
8785, 86sylibr 223 . . . . . . . . 9 (𝑓: 𝐴1-1-onto→(card‘𝑇) → 𝑥𝐴 (𝑓𝑥) ⊆ (card‘𝑇))
88 fof 6028 . . . . . . . . . . . 12 (𝑓: 𝐴onto→(card‘𝑇) → 𝑓: 𝐴⟶(card‘𝑇))
89 foelrn 6286 . . . . . . . . . . . . 13 ((𝑓: 𝐴onto→(card‘𝑇) ∧ 𝑦 ∈ (card‘𝑇)) → ∃𝑧 𝐴𝑦 = (𝑓𝑧))
9089ex 449 . . . . . . . . . . . 12 (𝑓: 𝐴onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → ∃𝑧 𝐴𝑦 = (𝑓𝑧)))
91 eluni2 4376 . . . . . . . . . . . . . . 15 (𝑧 𝐴 ↔ ∃𝑥𝐴 𝑧𝑥)
92 nfv 1830 . . . . . . . . . . . . . . . 16 𝑥 𝑓: 𝐴⟶(card‘𝑇)
93 nfiu1 4486 . . . . . . . . . . . . . . . . 17 𝑥 𝑥𝐴 (𝑓𝑥)
9493nfel2 2767 . . . . . . . . . . . . . . . 16 𝑥(𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥)
95 ssiun2 4499 . . . . . . . . . . . . . . . . . . 19 (𝑥𝐴 → (𝑓𝑥) ⊆ 𝑥𝐴 (𝑓𝑥))
96953ad2ant2 1076 . . . . . . . . . . . . . . . . . 18 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → (𝑓𝑥) ⊆ 𝑥𝐴 (𝑓𝑥))
97 ffn 5958 . . . . . . . . . . . . . . . . . . . 20 (𝑓: 𝐴⟶(card‘𝑇) → 𝑓 Fn 𝐴)
98973ad2ant1 1075 . . . . . . . . . . . . . . . . . . 19 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → 𝑓 Fn 𝐴)
99513ad2ant2 1076 . . . . . . . . . . . . . . . . . . 19 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → 𝑥 𝐴)
100 simp3 1056 . . . . . . . . . . . . . . . . . . 19 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → 𝑧𝑥)
101 fnfvima 6400 . . . . . . . . . . . . . . . . . . 19 ((𝑓 Fn 𝐴𝑥 𝐴𝑧𝑥) → (𝑓𝑧) ∈ (𝑓𝑥))
10298, 99, 100, 101syl3anc 1318 . . . . . . . . . . . . . . . . . 18 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → (𝑓𝑧) ∈ (𝑓𝑥))
10396, 102sseldd 3569 . . . . . . . . . . . . . . . . 17 ((𝑓: 𝐴⟶(card‘𝑇) ∧ 𝑥𝐴𝑧𝑥) → (𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥))
1041033exp 1256 . . . . . . . . . . . . . . . 16 (𝑓: 𝐴⟶(card‘𝑇) → (𝑥𝐴 → (𝑧𝑥 → (𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥))))
10592, 94, 104rexlimd 3008 . . . . . . . . . . . . . . 15 (𝑓: 𝐴⟶(card‘𝑇) → (∃𝑥𝐴 𝑧𝑥 → (𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥)))
10691, 105syl5bi 231 . . . . . . . . . . . . . 14 (𝑓: 𝐴⟶(card‘𝑇) → (𝑧 𝐴 → (𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥)))
107 eleq1a 2683 . . . . . . . . . . . . . 14 ((𝑓𝑧) ∈ 𝑥𝐴 (𝑓𝑥) → (𝑦 = (𝑓𝑧) → 𝑦 𝑥𝐴 (𝑓𝑥)))
108106, 107syl6 34 . . . . . . . . . . . . 13 (𝑓: 𝐴⟶(card‘𝑇) → (𝑧 𝐴 → (𝑦 = (𝑓𝑧) → 𝑦 𝑥𝐴 (𝑓𝑥))))
109108rexlimdv 3012 . . . . . . . . . . . 12 (𝑓: 𝐴⟶(card‘𝑇) → (∃𝑧 𝐴𝑦 = (𝑓𝑧) → 𝑦 𝑥𝐴 (𝑓𝑥)))
11088, 90, 109sylsyld 59 . . . . . . . . . . 11 (𝑓: 𝐴onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → 𝑦 𝑥𝐴 (𝑓𝑥)))
11145, 110syl 17 . . . . . . . . . 10 (𝑓: 𝐴1-1-onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → 𝑦 𝑥𝐴 (𝑓𝑥)))
112111ssrdv 3574 . . . . . . . . 9 (𝑓: 𝐴1-1-onto→(card‘𝑇) → (card‘𝑇) ⊆ 𝑥𝐴 (𝑓𝑥))
11387, 112eqssd 3585 . . . . . . . 8 (𝑓: 𝐴1-1-onto→(card‘𝑇) → 𝑥𝐴 (𝑓𝑥) = (card‘𝑇))
11484, 113syl5eqr 2658 . . . . . . 7 (𝑓: 𝐴1-1-onto→(card‘𝑇) → {𝑧 ∣ ∃𝑥𝐴 𝑧 = (𝑓𝑥)} = (card‘𝑇))
115114necon3ai 2807 . . . . . 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 1851 . . 3 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → ¬ ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇))
119 entr 7894 . . . . . . 7 (( 𝐴𝑇𝑇 ≈ (card‘𝑇)) → 𝐴 ≈ (card‘𝑇))
1203, 119sylan2 490 . . . . . 6 (( 𝐴𝑇𝑇 ∈ Tarski) → 𝐴 ≈ (card‘𝑇))
121 bren 7850 . . . . . 6 ( 𝐴 ≈ (card‘𝑇) ↔ ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇))
122120, 121sylib 207 . . . . 5 (( 𝐴𝑇𝑇 ∈ Tarski) → ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇))
123122expcom 450 . . . 4 (𝑇 ∈ Tarski → ( 𝐴𝑇 → ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇)))
1241233ad2ant1 1075 . . 3 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → ( 𝐴𝑇 → ∃𝑓 𝑓: 𝐴1-1-onto→(card‘𝑇)))
125118, 124mtod 188 . 2 ((𝑇 ∈ Tarski ∧ Tr 𝑇𝐴𝑇) → ¬ 𝐴𝑇)
126 uniss 4394 . . . . . . . . 9 (𝐴𝑇 𝐴 𝑇)
127 df-tr 4681 . . . . . . . . . 10 (Tr 𝑇 𝑇𝑇)
128127biimpi 205 . . . . . . . . 9 (Tr 𝑇 𝑇𝑇)
129126, 128sylan9ss 3581 . . . . . . . 8 ((𝐴𝑇 ∧ Tr 𝑇) → 𝐴𝑇)
130129expcom 450 . . . . . . 7 (Tr 𝑇 → (𝐴𝑇 𝐴𝑇))
13157, 130syld 46 . . . . . 6 (Tr 𝑇 → (𝐴𝑇 𝐴𝑇))
132131imp 444 . . . . 5 ((Tr 𝑇𝐴𝑇) → 𝐴𝑇)
133 tsken 9455 . . . . 5 ((𝑇 ∈ Tarski ∧ 𝐴𝑇) → ( 𝐴𝑇 𝐴𝑇))
134132, 133sylan2 490 . . . 4 ((𝑇 ∈ Tarski ∧ (Tr 𝑇𝐴𝑇)) → ( 𝐴𝑇 𝐴𝑇))
1351343impb 1252 . . 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 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  ∪ cuni 4372  ∪ ciun 4455   class class class wbr 4583   ↦ cmpt 4643  Tr wtr 4680  dom cdm 5038  ran crn 5039   “ cima 5041  Oncon0 5640  Lim wlim 5641   Fn wfn 5799  ⟶wf 5800  –1-1→wf1 5801  –onto→wfo 5802  –1-1-onto→wf1o 5803  ‘cfv 5804   ≈ cen 7838   ≼ cdom 7839   ≺ csdm 7840  cardccrd 8644  cfccf 8646  Inaccwcwina 9383  Inacccina 9384  Tarskictsk 9449 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-inf2 8421  ax-ac2 9168 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-smo 7330  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-oi 8298  df-har 8346  df-r1 8510  df-card 8648  df-aleph 8649  df-cf 8650  df-acn 8651  df-ac 8822  df-wina 9385  df-ina 9386  df-tsk 9450 This theorem is referenced by:  tskwun  9485  tskint  9486  tskun  9487  tskurn  9490  pwinfi3  36887
 Copyright terms: Public domain W3C validator