Step | Hyp | Ref
| Expression |
1 | | tsksdom 9457 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → 𝐴 ≺ 𝑇) |
2 | | cardidg 9249 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ Tarski →
(card‘𝑇) ≈
𝑇) |
3 | 2 | ensymd 7893 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ Tarski → 𝑇 ≈ (card‘𝑇)) |
4 | 3 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → 𝑇 ≈ (card‘𝑇)) |
5 | | sdomentr 7979 |
. . . . . . . . . . . 12
⊢ ((𝐴 ≺ 𝑇 ∧ 𝑇 ≈ (card‘𝑇)) → 𝐴 ≺ (card‘𝑇)) |
6 | 1, 4, 5 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → 𝐴 ≺ (card‘𝑇)) |
7 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) |
8 | 7 | rnmpt 5292 |
. . . . . . . . . . . . . 14
⊢ ran
(𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} |
9 | | cardon 8653 |
. . . . . . . . . . . . . . . . 17
⊢
(card‘𝑇)
∈ On |
10 | | sdomdom 7869 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ≺ (card‘𝑇) → 𝐴 ≼ (card‘𝑇)) |
11 | | ondomen 8743 |
. . . . . . . . . . . . . . . . 17
⊢
(((card‘𝑇)
∈ On ∧ 𝐴 ≼
(card‘𝑇)) →
𝐴 ∈ dom
card) |
12 | 9, 10, 11 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ≺ (card‘𝑇) → 𝐴 ∈ dom card) |
13 | 12 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑇 ∧ 𝐴 ≺ (card‘𝑇)) → 𝐴 ∈ dom card) |
14 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑓 ∈ V |
15 | 14 | imaex 6996 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 “ 𝑥) ∈ V |
16 | 15, 7 | fnmpti 5935 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) Fn 𝐴 |
17 | | dffn4 6034 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)):𝐴–onto→ran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥))) |
18 | 16, 17 | mpbi 219 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)):𝐴–onto→ran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) |
19 | | fodomnum 8763 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom card → ((𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)):𝐴–onto→ran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) → ran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) ≼ 𝐴)) |
20 | 13, 18, 19 | mpisyl 21 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑇 ∧ 𝐴 ≺ (card‘𝑇)) → ran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) ≼ 𝐴) |
21 | 8, 20 | syl5eqbrr 4619 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑇 ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≼ 𝐴) |
22 | | domsdomtr 7980 |
. . . . . . . . . . . . 13
⊢ (({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≼ 𝐴 ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (card‘𝑇)) |
23 | 21, 22 | sylancom 698 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑇 ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (card‘𝑇)) |
24 | 23 | adantll 746 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (card‘𝑇)) |
25 | 6, 24 | mpdan 699 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (card‘𝑇)) |
26 | | ne0i 3880 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑇 → 𝑇 ≠ ∅) |
27 | | tskcard 9482 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
(card‘𝑇) ∈
Inacc) |
28 | 26, 27 | sylan2 490 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → (card‘𝑇) ∈ Inacc) |
29 | | elina 9388 |
. . . . . . . . . . . 12
⊢
((card‘𝑇)
∈ Inacc ↔ ((card‘𝑇) ≠ ∅ ∧
(cf‘(card‘𝑇)) =
(card‘𝑇) ∧
∀𝑥 ∈
(card‘𝑇)𝒫
𝑥 ≺ (card‘𝑇))) |
30 | 29 | simp2bi 1070 |
. . . . . . . . . . 11
⊢
((card‘𝑇)
∈ Inacc → (cf‘(card‘𝑇)) = (card‘𝑇)) |
31 | 28, 30 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → (cf‘(card‘𝑇)) = (card‘𝑇)) |
32 | 25, 31 | breqtrrd 4611 |
. . . . . . . . 9
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (cf‘(card‘𝑇))) |
33 | 32 | 3adant2 1073 |
. . . . . . . 8
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (cf‘(card‘𝑇))) |
34 | 33 | adantr 480 |
. . . . . . 7
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (cf‘(card‘𝑇))) |
35 | 28 | 3adant2 1073 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → (card‘𝑇) ∈ Inacc) |
36 | 35 | adantr 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‘𝑇)) |
39 | 36, 37, 38 | 3syl 18 |
. . . . . . . 8
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → Lim (card‘𝑇)) |
40 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
41 | | eqeq1 2614 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → (𝑧 = (𝑓 “ 𝑥) ↔ 𝑦 = (𝑓 “ 𝑥))) |
42 | 41 | rexbidv 3034 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → (∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥) ↔ ∃𝑥 ∈ 𝐴 𝑦 = (𝑓 “ 𝑥))) |
43 | 40, 42 | elab 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‘𝑇)) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → ran 𝑓 = (card‘𝑇)) |
48 | 44, 47 | syl5sseq 3616 |
. . . . . . . . . . . . 13
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → (𝑓 “ 𝑥) ⊆ (card‘𝑇)) |
49 | 48 | ad2antlr 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 |
53 | 52 | f1imaen 7904 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:∪
𝐴–1-1→(card‘𝑇) ∧ 𝑥 ⊆ ∪ 𝐴) → (𝑓 “ 𝑥) ≈ 𝑥) |
54 | 50, 51, 53 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:∪
𝐴–1-1-onto→(card‘𝑇) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ 𝑥) ≈ 𝑥) |
55 | 54 | adantll 746 |
. . . . . . . . . . . . . 14
⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ 𝑥) ≈ 𝑥) |
56 | | simpl1 1057 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑇 ∈ Tarski) |
57 | | trss 4689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Tr 𝑇 → (𝐴 ∈ 𝑇 → 𝐴 ⊆ 𝑇)) |
58 | 57 | imp 444 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Tr
𝑇 ∧ 𝐴 ∈ 𝑇) → 𝐴 ⊆ 𝑇) |
59 | 58 | 3adant1 1072 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → 𝐴 ⊆ 𝑇) |
60 | 59 | sselda 3568 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑇) |
61 | | tsksdom 9457 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇) → 𝑥 ≺ 𝑇) |
62 | 56, 60, 61 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ 𝑇) |
63 | 56, 3 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑇 ≈ (card‘𝑇)) |
64 | | sdomentr 7979 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ≺ 𝑇 ∧ 𝑇 ≈ (card‘𝑇)) → 𝑥 ≺ (card‘𝑇)) |
65 | 62, 63, 64 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ (card‘𝑇)) |
66 | 65 | adantlr 747 |
. . . . . . . . . . . . . 14
⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ (card‘𝑇)) |
67 | | ensdomtr 7981 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 “ 𝑥) ≈ 𝑥 ∧ 𝑥 ≺ (card‘𝑇)) → (𝑓 “ 𝑥) ≺ (card‘𝑇)) |
68 | 55, 66, 67 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ 𝑥) ≺ (card‘𝑇)) |
69 | 36, 30 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → (cf‘(card‘𝑇)) = (card‘𝑇)) |
70 | 69 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (cf‘(card‘𝑇)) = (card‘𝑇)) |
71 | 68, 70 | breqtrrd 4611 |
. . . . . . . . . . . 12
⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ 𝑥) ≺ (cf‘(card‘𝑇))) |
72 | | sseq1 3589 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑓 “ 𝑥) → (𝑦 ⊆ (card‘𝑇) ↔ (𝑓 “ 𝑥) ⊆ (card‘𝑇))) |
73 | | breq1 4586 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑓 “ 𝑥) → (𝑦 ≺ (cf‘(card‘𝑇)) ↔ (𝑓 “ 𝑥) ≺ (cf‘(card‘𝑇)))) |
74 | 72, 73 | anbi12d 743 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑓 “ 𝑥) → ((𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))) ↔ ((𝑓 “ 𝑥) ⊆ (card‘𝑇) ∧ (𝑓 “ 𝑥) ≺ (cf‘(card‘𝑇))))) |
75 | 74 | biimprcd 239 |
. . . . . . . . . . . 12
⊢ (((𝑓 “ 𝑥) ⊆ (card‘𝑇) ∧ (𝑓 “ 𝑥) ≺ (cf‘(card‘𝑇))) → (𝑦 = (𝑓 “ 𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))))) |
76 | 49, 71, 75 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝑓 “ 𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))))) |
77 | 76 | rexlimdva 3013 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → (∃𝑥 ∈ 𝐴 𝑦 = (𝑓 “ 𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))))) |
78 | 43, 77 | syl5bi 231 |
. . . . . . . . 9
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → (𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))))) |
79 | 78 | ralrimiv 2948 |
. . . . . . . 8
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → ∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))) |
80 | | fvex 6113 |
. . . . . . . . 9
⊢
(card‘𝑇)
∈ V |
81 | 80 | cfslb2n 8973 |
. . . . . . . 8
⊢ ((Lim
(card‘𝑇) ∧
∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))) → ({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (cf‘(card‘𝑇)) → ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝑓 “ 𝑥)} ≠ (card‘𝑇))) |
82 | 39, 79, 81 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → ({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (cf‘(card‘𝑇)) → ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝑓 “ 𝑥)} ≠ (card‘𝑇))) |
83 | 34, 82 | mpd 15 |
. . . . . 6
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → ∪
{𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≠ (card‘𝑇)) |
84 | 15 | dfiun2 4490 |
. . . . . . . 8
⊢ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥) = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} |
85 | 48 | ralrimivw 2950 |
. . . . . . . . . 10
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → ∀𝑥 ∈ 𝐴 (𝑓 “ 𝑥) ⊆ (card‘𝑇)) |
86 | | iunss 4497 |
. . . . . . . . . 10
⊢ (∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥) ⊆ (card‘𝑇) ↔ ∀𝑥 ∈ 𝐴 (𝑓 “ 𝑥) ⊆ (card‘𝑇)) |
87 | 85, 86 | sylibr 223 |
. . . . . . . . 9
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥) ⊆ (card‘𝑇)) |
88 | | fof 6028 |
. . . . . . . . . . . 12
⊢ (𝑓:∪
𝐴–onto→(card‘𝑇) → 𝑓:∪ 𝐴⟶(card‘𝑇)) |
89 | | foelrn 6286 |
. . . . . . . . . . . . 13
⊢ ((𝑓:∪
𝐴–onto→(card‘𝑇) ∧ 𝑦 ∈ (card‘𝑇)) → ∃𝑧 ∈ ∪ 𝐴𝑦 = (𝑓‘𝑧)) |
90 | 89 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑓:∪
𝐴–onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → ∃𝑧 ∈ ∪ 𝐴𝑦 = (𝑓‘𝑧))) |
91 | | eluni2 4376 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ∪ 𝐴
↔ ∃𝑥 ∈
𝐴 𝑧 ∈ 𝑥) |
92 | | nfv 1830 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝑓:∪
𝐴⟶(card‘𝑇) |
93 | | nfiu1 4486 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥) |
94 | 93 | nfel2 2767 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝑓‘𝑧) ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥) |
95 | | ssiun2 4499 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐴 → (𝑓 “ 𝑥) ⊆ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥)) |
96 | 95 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:∪
𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (𝑓 “ 𝑥) ⊆ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥)) |
97 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓:∪
𝐴⟶(card‘𝑇) → 𝑓 Fn ∪ 𝐴) |
98 | 97 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:∪
𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → 𝑓 Fn ∪ 𝐴) |
99 | 51 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:∪
𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → 𝑥 ⊆ ∪ 𝐴) |
100 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:∪
𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝑥) |
101 | | fnfvima 6400 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 Fn ∪
𝐴 ∧ 𝑥 ⊆ ∪ 𝐴 ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ (𝑓 “ 𝑥)) |
102 | 98, 99, 100, 101 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:∪
𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ (𝑓 “ 𝑥)) |
103 | 96, 102 | sseldd 3569 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:∪
𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥)) |
104 | 103 | 3exp 1256 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:∪
𝐴⟶(card‘𝑇) → (𝑥 ∈ 𝐴 → (𝑧 ∈ 𝑥 → (𝑓‘𝑧) ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥)))) |
105 | 92, 94, 104 | rexlimd 3008 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:∪
𝐴⟶(card‘𝑇) → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝑥 → (𝑓‘𝑧) ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥))) |
106 | 91, 105 | syl5bi 231 |
. . . . . . . . . . . . . 14
⊢ (𝑓:∪
𝐴⟶(card‘𝑇) → (𝑧 ∈ ∪ 𝐴 → (𝑓‘𝑧) ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥))) |
107 | | eleq1a 2683 |
. . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑧) ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥) → (𝑦 = (𝑓‘𝑧) → 𝑦 ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥))) |
108 | 106, 107 | syl6 34 |
. . . . . . . . . . . . 13
⊢ (𝑓:∪
𝐴⟶(card‘𝑇) → (𝑧 ∈ ∪ 𝐴 → (𝑦 = (𝑓‘𝑧) → 𝑦 ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥)))) |
109 | 108 | rexlimdv 3012 |
. . . . . . . . . . . 12
⊢ (𝑓:∪
𝐴⟶(card‘𝑇) → (∃𝑧 ∈ ∪ 𝐴𝑦 = (𝑓‘𝑧) → 𝑦 ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥))) |
110 | 88, 90, 109 | sylsyld 59 |
. . . . . . . . . . 11
⊢ (𝑓:∪
𝐴–onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → 𝑦 ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥))) |
111 | 45, 110 | syl 17 |
. . . . . . . . . 10
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → 𝑦 ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥))) |
112 | 111 | ssrdv 3574 |
. . . . . . . . 9
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → (card‘𝑇) ⊆ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥)) |
113 | 87, 112 | eqssd 3585 |
. . . . . . . 8
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥) = (card‘𝑇)) |
114 | 84, 113 | syl5eqr 2658 |
. . . . . . 7
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} = (card‘𝑇)) |
115 | 114 | necon3ai 2807 |
. . . . . 6
⊢ (∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝑓 “ 𝑥)} ≠ (card‘𝑇) → ¬ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) |
116 | 83, 115 | syl 17 |
. . . . 5
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → ¬ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) |
117 | 116 | pm2.01da 457 |
. . . 4
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ¬ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) |
118 | 117 | nexdv 1851 |
. . 3
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ¬ ∃𝑓 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) |
119 | | entr 7894 |
. . . . . . 7
⊢ ((∪ 𝐴
≈ 𝑇 ∧ 𝑇 ≈ (card‘𝑇)) → ∪ 𝐴
≈ (card‘𝑇)) |
120 | 3, 119 | sylan2 490 |
. . . . . 6
⊢ ((∪ 𝐴
≈ 𝑇 ∧ 𝑇 ∈ Tarski) → ∪ 𝐴
≈ (card‘𝑇)) |
121 | | bren 7850 |
. . . . . 6
⊢ (∪ 𝐴
≈ (card‘𝑇)
↔ ∃𝑓 𝑓:∪
𝐴–1-1-onto→(card‘𝑇)) |
122 | 120, 121 | sylib 207 |
. . . . 5
⊢ ((∪ 𝐴
≈ 𝑇 ∧ 𝑇 ∈ Tarski) →
∃𝑓 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) |
123 | 122 | expcom 450 |
. . . 4
⊢ (𝑇 ∈ Tarski → (∪ 𝐴
≈ 𝑇 →
∃𝑓 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇))) |
124 | 123 | 3ad2ant1 1075 |
. . 3
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → (∪ 𝐴 ≈ 𝑇 → ∃𝑓 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇))) |
125 | 118, 124 | mtod 188 |
. 2
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ¬ ∪
𝐴 ≈ 𝑇) |
126 | | uniss 4394 |
. . . . . . . . 9
⊢ (𝐴 ⊆ 𝑇 → ∪ 𝐴 ⊆ ∪ 𝑇) |
127 | | df-tr 4681 |
. . . . . . . . . 10
⊢ (Tr 𝑇 ↔ ∪ 𝑇
⊆ 𝑇) |
128 | 127 | biimpi 205 |
. . . . . . . . 9
⊢ (Tr 𝑇 → ∪ 𝑇
⊆ 𝑇) |
129 | 126, 128 | sylan9ss 3581 |
. . . . . . . 8
⊢ ((𝐴 ⊆ 𝑇 ∧ Tr 𝑇) → ∪ 𝐴 ⊆ 𝑇) |
130 | 129 | expcom 450 |
. . . . . . 7
⊢ (Tr 𝑇 → (𝐴 ⊆ 𝑇 → ∪ 𝐴 ⊆ 𝑇)) |
131 | 57, 130 | syld 46 |
. . . . . 6
⊢ (Tr 𝑇 → (𝐴 ∈ 𝑇 → ∪ 𝐴 ⊆ 𝑇)) |
132 | 131 | imp 444 |
. . . . 5
⊢ ((Tr
𝑇 ∧ 𝐴 ∈ 𝑇) → ∪ 𝐴 ⊆ 𝑇) |
133 | | tsken 9455 |
. . . . 5
⊢ ((𝑇 ∈ Tarski ∧ ∪ 𝐴
⊆ 𝑇) → (∪ 𝐴
≈ 𝑇 ∨ ∪ 𝐴
∈ 𝑇)) |
134 | 132, 133 | sylan2 490 |
. . . 4
⊢ ((𝑇 ∈ Tarski ∧ (Tr 𝑇 ∧ 𝐴 ∈ 𝑇)) → (∪
𝐴 ≈ 𝑇 ∨ ∪ 𝐴 ∈ 𝑇)) |
135 | 134 | 3impb 1252 |
. . 3
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → (∪ 𝐴 ≈ 𝑇 ∨ ∪ 𝐴 ∈ 𝑇)) |
136 | 135 | ord 391 |
. 2
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → (¬ ∪
𝐴 ≈ 𝑇 → ∪ 𝐴 ∈ 𝑇)) |
137 | 125, 136 | mpd 15 |
1
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ∪ 𝐴 ∈ 𝑇) |