| Step | Hyp | Ref
| Expression |
| 1 | | tsksdom 10796 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → 𝐴 ≺ 𝑇) |
| 2 | | cardidg 10588 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ Tarski →
(card‘𝑇) ≈
𝑇) |
| 3 | 2 | ensymd 9045 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ Tarski → 𝑇 ≈ (card‘𝑇)) |
| 4 | 3 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → 𝑇 ≈ (card‘𝑇)) |
| 5 | | sdomentr 9151 |
. . . . . . . . . . . 12
⊢ ((𝐴 ≺ 𝑇 ∧ 𝑇 ≈ (card‘𝑇)) → 𝐴 ≺ (card‘𝑇)) |
| 6 | 1, 4, 5 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → 𝐴 ≺ (card‘𝑇)) |
| 7 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) |
| 8 | 7 | rnmpt 5968 |
. . . . . . . . . . . . . 14
⊢ ran
(𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} |
| 9 | | cardon 9984 |
. . . . . . . . . . . . . . . . 17
⊢
(card‘𝑇)
∈ On |
| 10 | | sdomdom 9020 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ≺ (card‘𝑇) → 𝐴 ≼ (card‘𝑇)) |
| 11 | | ondomen 10077 |
. . . . . . . . . . . . . . . . 17
⊢
(((card‘𝑇)
∈ On ∧ 𝐴 ≼
(card‘𝑇)) →
𝐴 ∈ dom
card) |
| 12 | 9, 10, 11 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ≺ (card‘𝑇) → 𝐴 ∈ dom card) |
| 13 | 12 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ 𝑇 ∧ 𝐴 ≺ (card‘𝑇)) → 𝐴 ∈ dom card) |
| 14 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑓 ∈ V |
| 15 | 14 | imaex 7936 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 “ 𝑥) ∈ V |
| 16 | 15, 7 | fnmpti 6711 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) Fn 𝐴 |
| 17 | | dffn4 6826 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)):𝐴–onto→ran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥))) |
| 18 | 16, 17 | mpbi 230 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)):𝐴–onto→ran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) |
| 19 | | fodomnum 10097 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom card → ((𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)):𝐴–onto→ran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) → ran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) ≼ 𝐴)) |
| 20 | 13, 18, 19 | mpisyl 21 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑇 ∧ 𝐴 ≺ (card‘𝑇)) → ran (𝑥 ∈ 𝐴 ↦ (𝑓 “ 𝑥)) ≼ 𝐴) |
| 21 | 8, 20 | eqbrtrrid 5179 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑇 ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≼ 𝐴) |
| 22 | | domsdomtr 9152 |
. . . . . . . . . . . . 13
⊢ (({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≼ 𝐴 ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (card‘𝑇)) |
| 23 | 21, 22 | sylancom 588 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑇 ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (card‘𝑇)) |
| 24 | 23 | adantll 714 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) ∧ 𝐴 ≺ (card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (card‘𝑇)) |
| 25 | 6, 24 | mpdan 687 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (card‘𝑇)) |
| 26 | | ne0i 4341 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑇 → 𝑇 ≠ ∅) |
| 27 | | tskcard 10821 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅) →
(card‘𝑇) ∈
Inacc) |
| 28 | 26, 27 | sylan2 593 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → (card‘𝑇) ∈ Inacc) |
| 29 | | elina 10727 |
. . . . . . . . . . . 12
⊢
((card‘𝑇)
∈ Inacc ↔ ((card‘𝑇) ≠ ∅ ∧
(cf‘(card‘𝑇)) =
(card‘𝑇) ∧
∀𝑥 ∈
(card‘𝑇)𝒫
𝑥 ≺ (card‘𝑇))) |
| 30 | 29 | simp2bi 1147 |
. . . . . . . . . . 11
⊢
((card‘𝑇)
∈ Inacc → (cf‘(card‘𝑇)) = (card‘𝑇)) |
| 31 | 28, 30 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → (cf‘(card‘𝑇)) = (card‘𝑇)) |
| 32 | 25, 31 | breqtrrd 5171 |
. . . . . . . . 9
⊢ ((𝑇 ∈ Tarski ∧ 𝐴 ∈ 𝑇) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (cf‘(card‘𝑇))) |
| 33 | 32 | 3adant2 1132 |
. . . . . . . 8
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (cf‘(card‘𝑇))) |
| 34 | 33 | adantr 480 |
. . . . . . 7
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (cf‘(card‘𝑇))) |
| 35 | 28 | 3adant2 1132 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → (card‘𝑇) ∈ Inacc) |
| 36 | 35 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → (card‘𝑇) ∈ Inacc) |
| 37 | | inawina 10730 |
. . . . . . . . 9
⊢
((card‘𝑇)
∈ Inacc → (card‘𝑇) ∈ Inaccw) |
| 38 | | winalim 10735 |
. . . . . . . . 9
⊢
((card‘𝑇)
∈ Inaccw → Lim (card‘𝑇)) |
| 39 | 36, 37, 38 | 3syl 18 |
. . . . . . . 8
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → Lim (card‘𝑇)) |
| 40 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
| 41 | | eqeq1 2741 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑦 → (𝑧 = (𝑓 “ 𝑥) ↔ 𝑦 = (𝑓 “ 𝑥))) |
| 42 | 41 | rexbidv 3179 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑦 → (∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥) ↔ ∃𝑥 ∈ 𝐴 𝑦 = (𝑓 “ 𝑥))) |
| 43 | 40, 42 | elab 3679 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ↔ ∃𝑥 ∈ 𝐴 𝑦 = (𝑓 “ 𝑥)) |
| 44 | | imassrn 6089 |
. . . . . . . . . . . . . 14
⊢ (𝑓 “ 𝑥) ⊆ ran 𝑓 |
| 45 | | f1ofo 6855 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → 𝑓:∪ 𝐴–onto→(card‘𝑇)) |
| 46 | | forn 6823 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:∪
𝐴–onto→(card‘𝑇) → ran 𝑓 = (card‘𝑇)) |
| 47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → ran 𝑓 = (card‘𝑇)) |
| 48 | 44, 47 | sseqtrid 4026 |
. . . . . . . . . . . . 13
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → (𝑓 “ 𝑥) ⊆ (card‘𝑇)) |
| 49 | 48 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ 𝑥) ⊆ (card‘𝑇)) |
| 50 | | f1of1 6847 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → 𝑓:∪ 𝐴–1-1→(card‘𝑇)) |
| 51 | | elssuni 4937 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴) |
| 52 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
| 53 | 52 | f1imaen 9057 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:∪
𝐴–1-1→(card‘𝑇) ∧ 𝑥 ⊆ ∪ 𝐴) → (𝑓 “ 𝑥) ≈ 𝑥) |
| 54 | 50, 51, 53 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:∪
𝐴–1-1-onto→(card‘𝑇) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ 𝑥) ≈ 𝑥) |
| 55 | 54 | adantll 714 |
. . . . . . . . . . . . . 14
⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ 𝑥) ≈ 𝑥) |
| 56 | | simpl1 1192 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑇 ∈ Tarski) |
| 57 | | trss 5270 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Tr 𝑇 → (𝐴 ∈ 𝑇 → 𝐴 ⊆ 𝑇)) |
| 58 | 57 | imp 406 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Tr
𝑇 ∧ 𝐴 ∈ 𝑇) → 𝐴 ⊆ 𝑇) |
| 59 | 58 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → 𝐴 ⊆ 𝑇) |
| 60 | 59 | sselda 3983 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝑇) |
| 61 | | tsksdom 10796 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇) → 𝑥 ≺ 𝑇) |
| 62 | 56, 60, 61 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ 𝑇) |
| 63 | 56, 3 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑇 ≈ (card‘𝑇)) |
| 64 | | sdomentr 9151 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ≺ 𝑇 ∧ 𝑇 ≈ (card‘𝑇)) → 𝑥 ≺ (card‘𝑇)) |
| 65 | 62, 63, 64 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ (card‘𝑇)) |
| 66 | 65 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≺ (card‘𝑇)) |
| 67 | | ensdomtr 9153 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 “ 𝑥) ≈ 𝑥 ∧ 𝑥 ≺ (card‘𝑇)) → (𝑓 “ 𝑥) ≺ (card‘𝑇)) |
| 68 | 55, 66, 67 | syl2anc 584 |
. . . . . . . . . . . . 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 5171 |
. . . . . . . . . . . 12
⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (𝑓 “ 𝑥) ≺ (cf‘(card‘𝑇))) |
| 72 | | sseq1 4009 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑓 “ 𝑥) → (𝑦 ⊆ (card‘𝑇) ↔ (𝑓 “ 𝑥) ⊆ (card‘𝑇))) |
| 73 | | breq1 5146 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑓 “ 𝑥) → (𝑦 ≺ (cf‘(card‘𝑇)) ↔ (𝑓 “ 𝑥) ≺ (cf‘(card‘𝑇)))) |
| 74 | 72, 73 | anbi12d 632 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝑓 “ 𝑥) → ((𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))) ↔ ((𝑓 “ 𝑥) ⊆ (card‘𝑇) ∧ (𝑓 “ 𝑥) ≺ (cf‘(card‘𝑇))))) |
| 75 | 74 | biimprcd 250 |
. . . . . . . . . . . 12
⊢ (((𝑓 “ 𝑥) ⊆ (card‘𝑇) ∧ (𝑓 “ 𝑥) ≺ (cf‘(card‘𝑇))) → (𝑦 = (𝑓 “ 𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))))) |
| 76 | 49, 71, 75 | syl2anc 584 |
. . . . . . . . . . 11
⊢ ((((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝑓 “ 𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))))) |
| 77 | 76 | rexlimdva 3155 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → (∃𝑥 ∈ 𝐴 𝑦 = (𝑓 “ 𝑥) → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))))) |
| 78 | 43, 77 | biimtrid 242 |
. . . . . . . . 9
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → (𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} → (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇))))) |
| 79 | 78 | ralrimiv 3145 |
. . . . . . . 8
⊢ (((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) ∧ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) → ∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))) |
| 80 | | fvex 6919 |
. . . . . . . . 9
⊢
(card‘𝑇)
∈ V |
| 81 | 80 | cfslb2n 10308 |
. . . . . . . 8
⊢ ((Lim
(card‘𝑇) ∧
∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} (𝑦 ⊆ (card‘𝑇) ∧ 𝑦 ≺ (cf‘(card‘𝑇)))) → ({𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} ≺ (cf‘(card‘𝑇)) → ∪ {𝑧
∣ ∃𝑥 ∈
𝐴 𝑧 = (𝑓 “ 𝑥)} ≠ (card‘𝑇))) |
| 82 | 39, 79, 81 | syl2anc 584 |
. . . . . . 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 5033 |
. . . . . . . 8
⊢ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥) = ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} |
| 85 | 48 | ralrimivw 3150 |
. . . . . . . . . 10
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → ∀𝑥 ∈ 𝐴 (𝑓 “ 𝑥) ⊆ (card‘𝑇)) |
| 86 | | iunss 5045 |
. . . . . . . . . 10
⊢ (∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥) ⊆ (card‘𝑇) ↔ ∀𝑥 ∈ 𝐴 (𝑓 “ 𝑥) ⊆ (card‘𝑇)) |
| 87 | 85, 86 | sylibr 234 |
. . . . . . . . 9
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥) ⊆ (card‘𝑇)) |
| 88 | | fof 6820 |
. . . . . . . . . . . 12
⊢ (𝑓:∪
𝐴–onto→(card‘𝑇) → 𝑓:∪ 𝐴⟶(card‘𝑇)) |
| 89 | | foelrn 7127 |
. . . . . . . . . . . . 13
⊢ ((𝑓:∪
𝐴–onto→(card‘𝑇) ∧ 𝑦 ∈ (card‘𝑇)) → ∃𝑧 ∈ ∪ 𝐴𝑦 = (𝑓‘𝑧)) |
| 90 | 89 | ex 412 |
. . . . . . . . . . . 12
⊢ (𝑓:∪
𝐴–onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → ∃𝑧 ∈ ∪ 𝐴𝑦 = (𝑓‘𝑧))) |
| 91 | | eluni2 4911 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ∪ 𝐴
↔ ∃𝑥 ∈
𝐴 𝑧 ∈ 𝑥) |
| 92 | | nfv 1914 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝑓:∪
𝐴⟶(card‘𝑇) |
| 93 | | nfiu1 5027 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥) |
| 94 | 93 | nfel2 2924 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥(𝑓‘𝑧) ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥) |
| 95 | | ssiun2 5047 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐴 → (𝑓 “ 𝑥) ⊆ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥)) |
| 96 | 95 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:∪
𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (𝑓 “ 𝑥) ⊆ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥)) |
| 97 | | ffn 6736 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓:∪
𝐴⟶(card‘𝑇) → 𝑓 Fn ∪ 𝐴) |
| 98 | 97 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:∪
𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → 𝑓 Fn ∪ 𝐴) |
| 99 | 51 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:∪
𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → 𝑥 ⊆ ∪ 𝐴) |
| 100 | | simp3 1139 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:∪
𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝑥) |
| 101 | | fnfvima 7253 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓 Fn ∪
𝐴 ∧ 𝑥 ⊆ ∪ 𝐴 ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ (𝑓 “ 𝑥)) |
| 102 | 98, 99, 100, 101 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:∪
𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ (𝑓 “ 𝑥)) |
| 103 | 96, 102 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:∪
𝐴⟶(card‘𝑇) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥)) |
| 104 | 103 | 3exp 1120 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:∪
𝐴⟶(card‘𝑇) → (𝑥 ∈ 𝐴 → (𝑧 ∈ 𝑥 → (𝑓‘𝑧) ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥)))) |
| 105 | 92, 94, 104 | rexlimd 3266 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:∪
𝐴⟶(card‘𝑇) → (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝑥 → (𝑓‘𝑧) ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥))) |
| 106 | 91, 105 | biimtrid 242 |
. . . . . . . . . . . . . 14
⊢ (𝑓:∪
𝐴⟶(card‘𝑇) → (𝑧 ∈ ∪ 𝐴 → (𝑓‘𝑧) ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥))) |
| 107 | | eleq1a 2836 |
. . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑧) ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥) → (𝑦 = (𝑓‘𝑧) → 𝑦 ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥))) |
| 108 | 106, 107 | syl6 35 |
. . . . . . . . . . . . 13
⊢ (𝑓:∪
𝐴⟶(card‘𝑇) → (𝑧 ∈ ∪ 𝐴 → (𝑦 = (𝑓‘𝑧) → 𝑦 ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥)))) |
| 109 | 108 | rexlimdv 3153 |
. . . . . . . . . . . 12
⊢ (𝑓:∪
𝐴⟶(card‘𝑇) → (∃𝑧 ∈ ∪ 𝐴𝑦 = (𝑓‘𝑧) → 𝑦 ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥))) |
| 110 | 88, 90, 109 | sylsyld 61 |
. . . . . . . . . . 11
⊢ (𝑓:∪
𝐴–onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → 𝑦 ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥))) |
| 111 | 45, 110 | syl 17 |
. . . . . . . . . 10
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → (𝑦 ∈ (card‘𝑇) → 𝑦 ∈ ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥))) |
| 112 | 111 | ssrdv 3989 |
. . . . . . . . 9
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → (card‘𝑇) ⊆ ∪ 𝑥 ∈ 𝐴 (𝑓 “ 𝑥)) |
| 113 | 87, 112 | eqssd 4001 |
. . . . . . . 8
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → ∪
𝑥 ∈ 𝐴 (𝑓 “ 𝑥) = (card‘𝑇)) |
| 114 | 84, 113 | eqtr3id 2791 |
. . . . . . 7
⊢ (𝑓:∪
𝐴–1-1-onto→(card‘𝑇) → ∪ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = (𝑓 “ 𝑥)} = (card‘𝑇)) |
| 115 | 114 | necon3ai 2965 |
. . . . . 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 799 |
. . . 4
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ¬ 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) |
| 118 | 117 | nexdv 1936 |
. . 3
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ¬ ∃𝑓 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) |
| 119 | | entr 9046 |
. . . . . . 7
⊢ ((∪ 𝐴
≈ 𝑇 ∧ 𝑇 ≈ (card‘𝑇)) → ∪ 𝐴
≈ (card‘𝑇)) |
| 120 | 3, 119 | sylan2 593 |
. . . . . 6
⊢ ((∪ 𝐴
≈ 𝑇 ∧ 𝑇 ∈ Tarski) → ∪ 𝐴
≈ (card‘𝑇)) |
| 121 | | bren 8995 |
. . . . . 6
⊢ (∪ 𝐴
≈ (card‘𝑇)
↔ ∃𝑓 𝑓:∪
𝐴–1-1-onto→(card‘𝑇)) |
| 122 | 120, 121 | sylib 218 |
. . . . 5
⊢ ((∪ 𝐴
≈ 𝑇 ∧ 𝑇 ∈ Tarski) →
∃𝑓 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇)) |
| 123 | 122 | expcom 413 |
. . . 4
⊢ (𝑇 ∈ Tarski → (∪ 𝐴
≈ 𝑇 →
∃𝑓 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇))) |
| 124 | 123 | 3ad2ant1 1134 |
. . 3
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → (∪ 𝐴 ≈ 𝑇 → ∃𝑓 𝑓:∪ 𝐴–1-1-onto→(card‘𝑇))) |
| 125 | 118, 124 | mtod 198 |
. 2
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ¬ ∪
𝐴 ≈ 𝑇) |
| 126 | | uniss 4915 |
. . . . . . . . 9
⊢ (𝐴 ⊆ 𝑇 → ∪ 𝐴 ⊆ ∪ 𝑇) |
| 127 | | df-tr 5260 |
. . . . . . . . . 10
⊢ (Tr 𝑇 ↔ ∪ 𝑇
⊆ 𝑇) |
| 128 | 127 | biimpi 216 |
. . . . . . . . 9
⊢ (Tr 𝑇 → ∪ 𝑇
⊆ 𝑇) |
| 129 | 126, 128 | sylan9ss 3997 |
. . . . . . . 8
⊢ ((𝐴 ⊆ 𝑇 ∧ Tr 𝑇) → ∪ 𝐴 ⊆ 𝑇) |
| 130 | 129 | expcom 413 |
. . . . . . 7
⊢ (Tr 𝑇 → (𝐴 ⊆ 𝑇 → ∪ 𝐴 ⊆ 𝑇)) |
| 131 | 57, 130 | syld 47 |
. . . . . 6
⊢ (Tr 𝑇 → (𝐴 ∈ 𝑇 → ∪ 𝐴 ⊆ 𝑇)) |
| 132 | 131 | imp 406 |
. . . . 5
⊢ ((Tr
𝑇 ∧ 𝐴 ∈ 𝑇) → ∪ 𝐴 ⊆ 𝑇) |
| 133 | | tsken 10794 |
. . . . 5
⊢ ((𝑇 ∈ Tarski ∧ ∪ 𝐴
⊆ 𝑇) → (∪ 𝐴
≈ 𝑇 ∨ ∪ 𝐴
∈ 𝑇)) |
| 134 | 132, 133 | sylan2 593 |
. . . 4
⊢ ((𝑇 ∈ Tarski ∧ (Tr 𝑇 ∧ 𝐴 ∈ 𝑇)) → (∪
𝐴 ≈ 𝑇 ∨ ∪ 𝐴 ∈ 𝑇)) |
| 135 | 134 | 3impb 1115 |
. . 3
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → (∪ 𝐴 ≈ 𝑇 ∨ ∪ 𝐴 ∈ 𝑇)) |
| 136 | 135 | ord 865 |
. 2
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → (¬ ∪
𝐴 ≈ 𝑇 → ∪ 𝐴 ∈ 𝑇)) |
| 137 | 125, 136 | mpd 15 |
1
⊢ ((𝑇 ∈ Tarski ∧ Tr 𝑇 ∧ 𝐴 ∈ 𝑇) → ∪ 𝐴 ∈ 𝑇) |