| Step | Hyp | Ref
| Expression |
| 1 | | brdom2 9022 |
. 2
⊢ (𝐴 ≼ ω ↔ (𝐴 ≺ ω ∨ 𝐴 ≈
ω)) |
| 2 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑔(𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) |
| 3 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑔∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)) |
| 4 | | isfinite2 9334 |
. . . . . . . . . 10
⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin) |
| 5 | | isfinite4 14401 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin ↔
(1...(♯‘𝐴))
≈ 𝐴) |
| 6 | 4, 5 | sylib 218 |
. . . . . . . . 9
⊢ (𝐴 ≺ ω →
(1...(♯‘𝐴))
≈ 𝐴) |
| 7 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) → (1...(♯‘𝐴)) ≈ 𝐴) |
| 8 | | bren 8995 |
. . . . . . . 8
⊢
((1...(♯‘𝐴)) ≈ 𝐴 ↔ ∃𝑔 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) |
| 9 | 7, 8 | sylib 218 |
. . . . . . 7
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) → ∃𝑔 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) |
| 10 | 9 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑔 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) |
| 11 | | f1of 6848 |
. . . . . . . . . . . 12
⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑔:(1...(♯‘𝐴))⟶𝐴) |
| 12 | 11 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝑔:(1...(♯‘𝐴))⟶𝐴) |
| 13 | | fconstmpt 5747 |
. . . . . . . . . . . . 13
⊢ ((ℕ
∖ (1...(♯‘𝐴))) × {𝑍}) = (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) |
| 14 | 13 | eqcomi 2746 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) = ((ℕ
∖ (1...(♯‘𝐴))) × {𝑍}) |
| 15 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝑍 ∈ 𝑉) |
| 16 | | fconst2g 7223 |
. . . . . . . . . . . . 13
⊢ (𝑍 ∈ 𝑉 → ((𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍):(ℕ ∖
(1...(♯‘𝐴)))⟶{𝑍} ↔ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) = ((ℕ
∖ (1...(♯‘𝐴))) × {𝑍}))) |
| 17 | 15, 16 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ((𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍):(ℕ ∖
(1...(♯‘𝐴)))⟶{𝑍} ↔ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) = ((ℕ
∖ (1...(♯‘𝐴))) × {𝑍}))) |
| 18 | 14, 17 | mpbiri 258 |
. . . . . . . . . . 11
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍):(ℕ ∖
(1...(♯‘𝐴)))⟶{𝑍}) |
| 19 | | disjdif 4472 |
. . . . . . . . . . . 12
⊢
((1...(♯‘𝐴)) ∩ (ℕ ∖
(1...(♯‘𝐴)))) =
∅ |
| 20 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) →
((1...(♯‘𝐴))
∩ (ℕ ∖ (1...(♯‘𝐴)))) = ∅) |
| 21 | | fun 6770 |
. . . . . . . . . . 11
⊢ (((𝑔:(1...(♯‘𝐴))⟶𝐴 ∧ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍):(ℕ ∖
(1...(♯‘𝐴)))⟶{𝑍}) ∧ ((1...(♯‘𝐴)) ∩ (ℕ ∖
(1...(♯‘𝐴)))) =
∅) → (𝑔 ∪
(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):((1...(♯‘𝐴)) ∪ (ℕ ∖
(1...(♯‘𝐴))))⟶(𝐴 ∪ {𝑍})) |
| 22 | 12, 18, 20, 21 | syl21anc 838 |
. . . . . . . . . 10
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):((1...(♯‘𝐴)) ∪ (ℕ ∖
(1...(♯‘𝐴))))⟶(𝐴 ∪ {𝑍})) |
| 23 | | fz1ssnn 13595 |
. . . . . . . . . . . 12
⊢
(1...(♯‘𝐴)) ⊆ ℕ |
| 24 | | undif 4482 |
. . . . . . . . . . . 12
⊢
((1...(♯‘𝐴)) ⊆ ℕ ↔
((1...(♯‘𝐴))
∪ (ℕ ∖ (1...(♯‘𝐴)))) = ℕ) |
| 25 | 23, 24 | mpbi 230 |
. . . . . . . . . . 11
⊢
((1...(♯‘𝐴)) ∪ (ℕ ∖
(1...(♯‘𝐴)))) =
ℕ |
| 26 | 25 | feq2i 6728 |
. . . . . . . . . 10
⊢ ((𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):((1...(♯‘𝐴)) ∪ (ℕ ∖
(1...(♯‘𝐴))))⟶(𝐴 ∪ {𝑍}) ↔ (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍})) |
| 27 | 22, 26 | sylib 218 |
. . . . . . . . 9
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍})) |
| 28 | 27 | 3adantl3 1169 |
. . . . . . . 8
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍})) |
| 29 | | ssid 4006 |
. . . . . . . . . . . . 13
⊢ 𝐴 ⊆ 𝐴 |
| 30 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) |
| 31 | | f1ofo 6855 |
. . . . . . . . . . . . . 14
⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑔:(1...(♯‘𝐴))–onto→𝐴) |
| 32 | | forn 6823 |
. . . . . . . . . . . . . 14
⊢ (𝑔:(1...(♯‘𝐴))–onto→𝐴 → ran 𝑔 = 𝐴) |
| 33 | 30, 31, 32 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ran 𝑔 = 𝐴) |
| 34 | 29, 33 | sseqtrrid 4027 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ ran 𝑔) |
| 35 | 34 | orcd 874 |
. . . . . . . . . . 11
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝐴 ⊆ ran 𝑔 ∨ 𝐴 ⊆ ran (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍))) |
| 36 | | ssun 4195 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ran 𝑔 ∨ 𝐴 ⊆ ran (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → 𝐴 ⊆ (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍))) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍))) |
| 38 | | rnun 6165 |
. . . . . . . . . 10
⊢ ran
(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) = (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) |
| 39 | 37, 38 | sseqtrrdi 4025 |
. . . . . . . . 9
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍))) |
| 40 | 39 | 3adantl3 1169 |
. . . . . . . 8
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍))) |
| 41 | | dff1o3 6854 |
. . . . . . . . . . 11
⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 ↔ (𝑔:(1...(♯‘𝐴))–onto→𝐴 ∧ Fun ◡𝑔)) |
| 42 | 41 | simprbi 496 |
. . . . . . . . . 10
⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → Fun ◡𝑔) |
| 43 | 42 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → Fun ◡𝑔) |
| 44 | | cnvun 6162 |
. . . . . . . . . . . . 13
⊢ ◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) = (◡𝑔 ∪ ◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) |
| 45 | 44 | reseq1i 5993 |
. . . . . . . . . . . 12
⊢ (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴) = ((◡𝑔 ∪ ◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴) |
| 46 | | resundir 6012 |
. . . . . . . . . . . 12
⊢ ((◡𝑔 ∪ ◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴) = ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ↾ 𝐴)) |
| 47 | 45, 46 | eqtri 2765 |
. . . . . . . . . . 11
⊢ (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴) = ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ↾ 𝐴)) |
| 48 | | dff1o4 6856 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 ↔ (𝑔 Fn (1...(♯‘𝐴)) ∧ ◡𝑔 Fn 𝐴)) |
| 49 | 48 | simprbi 496 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → ◡𝑔 Fn 𝐴) |
| 50 | | fnresdm 6687 |
. . . . . . . . . . . . . . 15
⊢ (◡𝑔 Fn 𝐴 → (◡𝑔 ↾ 𝐴) = ◡𝑔) |
| 51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → (◡𝑔 ↾ 𝐴) = ◡𝑔) |
| 52 | 51 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (◡𝑔 ↾ 𝐴) = ◡𝑔) |
| 53 | | simpl3 1194 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ¬ 𝑍 ∈ 𝐴) |
| 54 | 14 | cnveqi 5885 |
. . . . . . . . . . . . . . . . 17
⊢ ◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) = ◡((ℕ ∖ (1...(♯‘𝐴))) × {𝑍}) |
| 55 | | cnvxp 6177 |
. . . . . . . . . . . . . . . . 17
⊢ ◡((ℕ ∖ (1...(♯‘𝐴))) × {𝑍}) = ({𝑍} × (ℕ ∖
(1...(♯‘𝐴)))) |
| 56 | 54, 55 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
⊢ ◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) = ({𝑍} × (ℕ ∖
(1...(♯‘𝐴)))) |
| 57 | 56 | reseq1i 5993 |
. . . . . . . . . . . . . . 15
⊢ (◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ↾ 𝐴) = (({𝑍} × (ℕ ∖
(1...(♯‘𝐴))))
↾ 𝐴) |
| 58 | | incom 4209 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∩ {𝑍}) = ({𝑍} ∩ 𝐴) |
| 59 | | disjsn 4711 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∩ {𝑍}) = ∅ ↔ ¬ 𝑍 ∈ 𝐴) |
| 60 | 59 | biimpri 228 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑍 ∈ 𝐴 → (𝐴 ∩ {𝑍}) = ∅) |
| 61 | 58, 60 | eqtr3id 2791 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑍 ∈ 𝐴 → ({𝑍} ∩ 𝐴) = ∅) |
| 62 | | xpdisjres 32611 |
. . . . . . . . . . . . . . . 16
⊢ (({𝑍} ∩ 𝐴) = ∅ → (({𝑍} × (ℕ ∖
(1...(♯‘𝐴))))
↾ 𝐴) =
∅) |
| 63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑍 ∈ 𝐴 → (({𝑍} × (ℕ ∖
(1...(♯‘𝐴))))
↾ 𝐴) =
∅) |
| 64 | 57, 63 | eqtrid 2789 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑍 ∈ 𝐴 → (◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ↾ 𝐴) = ∅) |
| 65 | 53, 64 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ↾ 𝐴) = ∅) |
| 66 | 52, 65 | uneq12d 4169 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ↾ 𝐴)) = (◡𝑔 ∪ ∅)) |
| 67 | | un0 4394 |
. . . . . . . . . . . 12
⊢ (◡𝑔 ∪ ∅) = ◡𝑔 |
| 68 | 66, 67 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ↾ 𝐴)) = ◡𝑔) |
| 69 | 47, 68 | eqtrid 2789 |
. . . . . . . . . 10
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴) = ◡𝑔) |
| 70 | 69 | funeqd 6588 |
. . . . . . . . 9
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴) ↔ Fun ◡𝑔)) |
| 71 | 43, 70 | mpbird 257 |
. . . . . . . 8
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴)) |
| 72 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑔 ∈ V |
| 73 | | nnex 12272 |
. . . . . . . . . . . 12
⊢ ℕ
∈ V |
| 74 | | difexg 5329 |
. . . . . . . . . . . 12
⊢ (ℕ
∈ V → (ℕ ∖ (1...(♯‘𝐴))) ∈ V) |
| 75 | 73, 74 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ℕ
∖ (1...(♯‘𝐴))) ∈ V |
| 76 | 75 | mptex 7243 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ∈
V |
| 77 | 72, 76 | unex 7764 |
. . . . . . . . 9
⊢ (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ∈
V |
| 78 | | feq1 6716 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ↔ (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}))) |
| 79 | | rneq 5947 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → ran
𝑓 = ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍))) |
| 80 | 79 | sseq2d 4016 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → (𝐴 ⊆ ran 𝑓 ↔ 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)))) |
| 81 | | cnveq 5884 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → ◡𝑓 = ◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍))) |
| 82 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → 𝐴 = 𝐴) |
| 83 | 81, 82 | reseq12d 5998 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → (◡𝑓 ↾ 𝐴) = (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴)) |
| 84 | 83 | funeqd 6588 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → (Fun
(◡𝑓 ↾ 𝐴) ↔ Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴))) |
| 85 | 78, 80, 84 | 3anbi123d 1438 |
. . . . . . . . 9
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → ((𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)) ↔ ((𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ∧ Fun
(◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴)))) |
| 86 | 77, 85 | spcev 3606 |
. . . . . . . 8
⊢ (((𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ∧ Fun
(◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴)) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
| 87 | 28, 40, 71, 86 | syl3anc 1373 |
. . . . . . 7
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
| 88 | 87 | ex 412 |
. . . . . 6
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
| 89 | 2, 3, 10, 88 | exlimimdd 2219 |
. . . . 5
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
| 90 | 89 | 3expia 1122 |
. . . 4
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) → (¬ 𝑍 ∈ 𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
| 91 | | nnenom 14021 |
. . . . . . . 8
⊢ ℕ
≈ ω |
| 92 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → 𝐴 ≈ ω) |
| 93 | 92 | ensymd 9045 |
. . . . . . . 8
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ω ≈ 𝐴) |
| 94 | | entr 9046 |
. . . . . . . 8
⊢ ((ℕ
≈ ω ∧ ω ≈ 𝐴) → ℕ ≈ 𝐴) |
| 95 | 91, 93, 94 | sylancr 587 |
. . . . . . 7
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ℕ ≈ 𝐴) |
| 96 | | bren 8995 |
. . . . . . 7
⊢ (ℕ
≈ 𝐴 ↔
∃𝑓 𝑓:ℕ–1-1-onto→𝐴) |
| 97 | 95, 96 | sylib 218 |
. . . . . 6
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ∃𝑓 𝑓:ℕ–1-1-onto→𝐴) |
| 98 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑓(𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) |
| 99 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓:ℕ–1-1-onto→𝐴) |
| 100 | | f1of 6848 |
. . . . . . . . . 10
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:ℕ⟶𝐴) |
| 101 | | ssun1 4178 |
. . . . . . . . . . 11
⊢ 𝐴 ⊆ (𝐴 ∪ {𝑍}) |
| 102 | | fss 6752 |
. . . . . . . . . . 11
⊢ ((𝑓:ℕ⟶𝐴 ∧ 𝐴 ⊆ (𝐴 ∪ {𝑍})) → 𝑓:ℕ⟶(𝐴 ∪ {𝑍})) |
| 103 | 101, 102 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑓:ℕ⟶𝐴 → 𝑓:ℕ⟶(𝐴 ∪ {𝑍})) |
| 104 | 99, 100, 103 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓:ℕ⟶(𝐴 ∪ {𝑍})) |
| 105 | | f1ofo 6855 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:ℕ–onto→𝐴) |
| 106 | | forn 6823 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐴 → ran 𝑓 = 𝐴) |
| 107 | 99, 105, 106 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → ran 𝑓 = 𝐴) |
| 108 | 29, 107 | sseqtrrid 4027 |
. . . . . . . . 9
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝐴 ⊆ ran 𝑓) |
| 109 | | f1ocnv 6860 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→ℕ) |
| 110 | | f1of1 6847 |
. . . . . . . . . . 11
⊢ (◡𝑓:𝐴–1-1-onto→ℕ → ◡𝑓:𝐴–1-1→ℕ) |
| 111 | 99, 109, 110 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → ◡𝑓:𝐴–1-1→ℕ) |
| 112 | | f1ores 6862 |
. . . . . . . . . . 11
⊢ ((◡𝑓:𝐴–1-1→ℕ ∧ 𝐴 ⊆ 𝐴) → (◡𝑓 ↾ 𝐴):𝐴–1-1-onto→(◡𝑓 “ 𝐴)) |
| 113 | 29, 112 | mpan2 691 |
. . . . . . . . . 10
⊢ (◡𝑓:𝐴–1-1→ℕ → (◡𝑓 ↾ 𝐴):𝐴–1-1-onto→(◡𝑓 “ 𝐴)) |
| 114 | | f1ofun 6850 |
. . . . . . . . . 10
⊢ ((◡𝑓 ↾ 𝐴):𝐴–1-1-onto→(◡𝑓 “ 𝐴) → Fun (◡𝑓 ↾ 𝐴)) |
| 115 | 111, 113,
114 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → Fun (◡𝑓 ↾ 𝐴)) |
| 116 | 104, 108,
115 | 3jca 1129 |
. . . . . . . 8
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
| 117 | 116 | ex 412 |
. . . . . . 7
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → (𝑓:ℕ–1-1-onto→𝐴 → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
| 118 | 98, 117 | eximd 2216 |
. . . . . 6
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → (∃𝑓 𝑓:ℕ–1-1-onto→𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
| 119 | 97, 118 | mpd 15 |
. . . . 5
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
| 120 | 119 | a1d 25 |
. . . 4
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → (¬ 𝑍 ∈ 𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
| 121 | 90, 120 | jaoian 959 |
. . 3
⊢ (((𝐴 ≺ ω ∨ 𝐴 ≈ ω) ∧ 𝑍 ∈ 𝑉) → (¬ 𝑍 ∈ 𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
| 122 | 121 | 3impia 1118 |
. 2
⊢ (((𝐴 ≺ ω ∨ 𝐴 ≈ ω) ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
| 123 | 1, 122 | syl3an1b 1405 |
1
⊢ ((𝐴 ≼ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |