Step | Hyp | Ref
| Expression |
1 | | brdom2 8658 |
. 2
⊢ (𝐴 ≼ ω ↔ (𝐴 ≺ ω ∨ 𝐴 ≈
ω)) |
2 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑔(𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) |
3 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑔∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)) |
4 | | isfinite2 8929 |
. . . . . . . . . 10
⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin) |
5 | | isfinite4 13929 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin ↔
(1...(♯‘𝐴))
≈ 𝐴) |
6 | 4, 5 | sylib 221 |
. . . . . . . . 9
⊢ (𝐴 ≺ ω →
(1...(♯‘𝐴))
≈ 𝐴) |
7 | 6 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) → (1...(♯‘𝐴)) ≈ 𝐴) |
8 | | bren 8636 |
. . . . . . . 8
⊢
((1...(♯‘𝐴)) ≈ 𝐴 ↔ ∃𝑔 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) |
9 | 7, 8 | sylib 221 |
. . . . . . 7
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) → ∃𝑔 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) |
10 | 9 | 3adant3 1134 |
. . . . . 6
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑔 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) |
11 | | f1of 6661 |
. . . . . . . . . . . 12
⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑔:(1...(♯‘𝐴))⟶𝐴) |
12 | 11 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝑔:(1...(♯‘𝐴))⟶𝐴) |
13 | | fconstmpt 5611 |
. . . . . . . . . . . . 13
⊢ ((ℕ
∖ (1...(♯‘𝐴))) × {𝑍}) = (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) |
14 | 13 | eqcomi 2746 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) = ((ℕ
∖ (1...(♯‘𝐴))) × {𝑍}) |
15 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝑍 ∈ 𝑉) |
16 | | fconst2g 7018 |
. . . . . . . . . . . . 13
⊢ (𝑍 ∈ 𝑉 → ((𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍):(ℕ ∖
(1...(♯‘𝐴)))⟶{𝑍} ↔ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) = ((ℕ
∖ (1...(♯‘𝐴))) × {𝑍}))) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ((𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍):(ℕ ∖
(1...(♯‘𝐴)))⟶{𝑍} ↔ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) = ((ℕ
∖ (1...(♯‘𝐴))) × {𝑍}))) |
18 | 14, 17 | mpbiri 261 |
. . . . . . . . . . 11
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍):(ℕ ∖
(1...(♯‘𝐴)))⟶{𝑍}) |
19 | | disjdif 4386 |
. . . . . . . . . . . 12
⊢
((1...(♯‘𝐴)) ∩ (ℕ ∖
(1...(♯‘𝐴)))) =
∅ |
20 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) →
((1...(♯‘𝐴))
∩ (ℕ ∖ (1...(♯‘𝐴)))) = ∅) |
21 | | fun 6581 |
. . . . . . . . . . 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 13143 |
. . . . . . . . . . . 12
⊢
(1...(♯‘𝐴)) ⊆ ℕ |
24 | | undif 4396 |
. . . . . . . . . . . 12
⊢
((1...(♯‘𝐴)) ⊆ ℕ ↔
((1...(♯‘𝐴))
∪ (ℕ ∖ (1...(♯‘𝐴)))) = ℕ) |
25 | 23, 24 | mpbi 233 |
. . . . . . . . . . 11
⊢
((1...(♯‘𝐴)) ∪ (ℕ ∖
(1...(♯‘𝐴)))) =
ℕ |
26 | 25 | feq2i 6537 |
. . . . . . . . . 10
⊢ ((𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):((1...(♯‘𝐴)) ∪ (ℕ ∖
(1...(♯‘𝐴))))⟶(𝐴 ∪ {𝑍}) ↔ (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍})) |
27 | 22, 26 | sylib 221 |
. . . . . . . . 9
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍})) |
28 | 27 | 3adantl3 1170 |
. . . . . . . 8
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍})) |
29 | | ssid 3923 |
. . . . . . . . . . . . 13
⊢ 𝐴 ⊆ 𝐴 |
30 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) |
31 | | f1ofo 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → 𝑔:(1...(♯‘𝐴))–onto→𝐴) |
32 | | forn 6636 |
. . . . . . . . . . . . . 14
⊢ (𝑔:(1...(♯‘𝐴))–onto→𝐴 → ran 𝑔 = 𝐴) |
33 | 30, 31, 32 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ran 𝑔 = 𝐴) |
34 | 29, 33 | sseqtrrid 3954 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ ran 𝑔) |
35 | 34 | orcd 873 |
. . . . . . . . . . 11
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (𝐴 ⊆ ran 𝑔 ∨ 𝐴 ⊆ ran (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍))) |
36 | | ssun 4103 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ran 𝑔 ∨ 𝐴 ⊆ ran (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → 𝐴 ⊆ (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍))) |
38 | | rnun 6009 |
. . . . . . . . . 10
⊢ ran
(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) = (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) |
39 | 37, 38 | sseqtrrdi 3952 |
. . . . . . . . 9
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍))) |
40 | 39 | 3adantl3 1170 |
. . . . . . . 8
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍))) |
41 | | dff1o3 6667 |
. . . . . . . . . . 11
⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 ↔ (𝑔:(1...(♯‘𝐴))–onto→𝐴 ∧ Fun ◡𝑔)) |
42 | 41 | simprbi 500 |
. . . . . . . . . 10
⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → Fun ◡𝑔) |
43 | 42 | adantl 485 |
. . . . . . . . 9
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → Fun ◡𝑔) |
44 | | cnvun 6006 |
. . . . . . . . . . . . 13
⊢ ◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) = (◡𝑔 ∪ ◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) |
45 | 44 | reseq1i 5847 |
. . . . . . . . . . . 12
⊢ (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴) = ((◡𝑔 ∪ ◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴) |
46 | | resundir 5866 |
. . . . . . . . . . . 12
⊢ ((◡𝑔 ∪ ◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴) = ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ↾ 𝐴)) |
47 | 45, 46 | eqtri 2765 |
. . . . . . . . . . 11
⊢ (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴) = ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ↾ 𝐴)) |
48 | | dff1o4 6669 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 ↔ (𝑔 Fn (1...(♯‘𝐴)) ∧ ◡𝑔 Fn 𝐴)) |
49 | 48 | simprbi 500 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → ◡𝑔 Fn 𝐴) |
50 | | fnresdm 6496 |
. . . . . . . . . . . . . . 15
⊢ (◡𝑔 Fn 𝐴 → (◡𝑔 ↾ 𝐴) = ◡𝑔) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → (◡𝑔 ↾ 𝐴) = ◡𝑔) |
52 | 51 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (◡𝑔 ↾ 𝐴) = ◡𝑔) |
53 | | simpl3 1195 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ¬ 𝑍 ∈ 𝐴) |
54 | 14 | cnveqi 5743 |
. . . . . . . . . . . . . . . . 17
⊢ ◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) = ◡((ℕ ∖ (1...(♯‘𝐴))) × {𝑍}) |
55 | | cnvxp 6020 |
. . . . . . . . . . . . . . . . 17
⊢ ◡((ℕ ∖ (1...(♯‘𝐴))) × {𝑍}) = ({𝑍} × (ℕ ∖
(1...(♯‘𝐴)))) |
56 | 54, 55 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
⊢ ◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) = ({𝑍} × (ℕ ∖
(1...(♯‘𝐴)))) |
57 | 56 | reseq1i 5847 |
. . . . . . . . . . . . . . 15
⊢ (◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ↾ 𝐴) = (({𝑍} × (ℕ ∖
(1...(♯‘𝐴))))
↾ 𝐴) |
58 | | incom 4115 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∩ {𝑍}) = ({𝑍} ∩ 𝐴) |
59 | | disjsn 4627 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∩ {𝑍}) = ∅ ↔ ¬ 𝑍 ∈ 𝐴) |
60 | 59 | biimpri 231 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑍 ∈ 𝐴 → (𝐴 ∩ {𝑍}) = ∅) |
61 | 58, 60 | eqtr3id 2792 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑍 ∈ 𝐴 → ({𝑍} ∩ 𝐴) = ∅) |
62 | | xpdisjres 30656 |
. . . . . . . . . . . . . . . 16
⊢ (({𝑍} ∩ 𝐴) = ∅ → (({𝑍} × (ℕ ∖
(1...(♯‘𝐴))))
↾ 𝐴) =
∅) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑍 ∈ 𝐴 → (({𝑍} × (ℕ ∖
(1...(♯‘𝐴))))
↾ 𝐴) =
∅) |
64 | 57, 63 | syl5eq 2790 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑍 ∈ 𝐴 → (◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ↾ 𝐴) = ∅) |
65 | 53, 64 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ↾ 𝐴) = ∅) |
66 | 52, 65 | uneq12d 4078 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ↾ 𝐴)) = (◡𝑔 ∪ ∅)) |
67 | | un0 4305 |
. . . . . . . . . . . 12
⊢ (◡𝑔 ∪ ∅) = ◡𝑔 |
68 | 66, 67 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ↾ 𝐴)) = ◡𝑔) |
69 | 47, 68 | syl5eq 2790 |
. . . . . . . . . 10
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴) = ◡𝑔) |
70 | 69 | funeqd 6402 |
. . . . . . . . 9
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → (Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴) ↔ Fun ◡𝑔)) |
71 | 43, 70 | mpbird 260 |
. . . . . . . 8
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴) → Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴)) |
72 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑔 ∈ V |
73 | | nnex 11836 |
. . . . . . . . . . . 12
⊢ ℕ
∈ V |
74 | | difexg 5220 |
. . . . . . . . . . . 12
⊢ (ℕ
∈ V → (ℕ ∖ (1...(♯‘𝐴))) ∈ V) |
75 | 73, 74 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (ℕ
∖ (1...(♯‘𝐴))) ∈ V |
76 | 75 | mptex 7039 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍) ∈
V |
77 | 72, 76 | unex 7531 |
. . . . . . . . 9
⊢ (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ∈
V |
78 | | feq1 6526 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ↔ (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}))) |
79 | | rneq 5805 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → ran
𝑓 = ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍))) |
80 | 79 | sseq2d 3933 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → (𝐴 ⊆ ran 𝑓 ↔ 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)))) |
81 | | cnveq 5742 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → ◡𝑓 = ◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍))) |
82 | | eqidd 2738 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → 𝐴 = 𝐴) |
83 | 81, 82 | reseq12d 5852 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → (◡𝑓 ↾ 𝐴) = (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴)) |
84 | 83 | funeqd 6402 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → (Fun
(◡𝑓 ↾ 𝐴) ↔ Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴))) |
85 | 78, 80, 84 | 3anbi123d 1438 |
. . . . . . . . 9
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) → ((𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)) ↔ ((𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ∧ Fun
(◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(♯‘𝐴)))
↦ 𝑍)) ↾ 𝐴)))) |
86 | 77, 85 | spcev 3521 |
. . . . . . . 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 416 |
. . . . . 6
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → (𝑔:(1...(♯‘𝐴))–1-1-onto→𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
89 | 2, 3, 10, 88 | exlimimdd 2217 |
. . . . 5
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
90 | 89 | 3expia 1123 |
. . . 4
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) → (¬ 𝑍 ∈ 𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
91 | | nnenom 13553 |
. . . . . . . 8
⊢ ℕ
≈ ω |
92 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → 𝐴 ≈ ω) |
93 | 92 | ensymd 8679 |
. . . . . . . 8
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ω ≈ 𝐴) |
94 | | entr 8680 |
. . . . . . . 8
⊢ ((ℕ
≈ ω ∧ ω ≈ 𝐴) → ℕ ≈ 𝐴) |
95 | 91, 93, 94 | sylancr 590 |
. . . . . . 7
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ℕ ≈ 𝐴) |
96 | | bren 8636 |
. . . . . . 7
⊢ (ℕ
≈ 𝐴 ↔
∃𝑓 𝑓:ℕ–1-1-onto→𝐴) |
97 | 95, 96 | sylib 221 |
. . . . . 6
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ∃𝑓 𝑓:ℕ–1-1-onto→𝐴) |
98 | | nfv 1922 |
. . . . . . 7
⊢
Ⅎ𝑓(𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) |
99 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓:ℕ–1-1-onto→𝐴) |
100 | | f1of 6661 |
. . . . . . . . . 10
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:ℕ⟶𝐴) |
101 | | ssun1 4086 |
. . . . . . . . . . 11
⊢ 𝐴 ⊆ (𝐴 ∪ {𝑍}) |
102 | | fss 6562 |
. . . . . . . . . . 11
⊢ ((𝑓:ℕ⟶𝐴 ∧ 𝐴 ⊆ (𝐴 ∪ {𝑍})) → 𝑓:ℕ⟶(𝐴 ∪ {𝑍})) |
103 | 101, 102 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝑓:ℕ⟶𝐴 → 𝑓:ℕ⟶(𝐴 ∪ {𝑍})) |
104 | 99, 100, 103 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓:ℕ⟶(𝐴 ∪ {𝑍})) |
105 | | f1ofo 6668 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:ℕ–onto→𝐴) |
106 | | forn 6636 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐴 → ran 𝑓 = 𝐴) |
107 | 99, 105, 106 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → ran 𝑓 = 𝐴) |
108 | 29, 107 | sseqtrrid 3954 |
. . . . . . . . 9
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝐴 ⊆ ran 𝑓) |
109 | | f1ocnv 6673 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→ℕ) |
110 | | f1of1 6660 |
. . . . . . . . . . 11
⊢ (◡𝑓:𝐴–1-1-onto→ℕ → ◡𝑓:𝐴–1-1→ℕ) |
111 | 99, 109, 110 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → ◡𝑓:𝐴–1-1→ℕ) |
112 | | f1ores 6675 |
. . . . . . . . . . 11
⊢ ((◡𝑓:𝐴–1-1→ℕ ∧ 𝐴 ⊆ 𝐴) → (◡𝑓 ↾ 𝐴):𝐴–1-1-onto→(◡𝑓 “ 𝐴)) |
113 | 29, 112 | mpan2 691 |
. . . . . . . . . 10
⊢ (◡𝑓:𝐴–1-1→ℕ → (◡𝑓 ↾ 𝐴):𝐴–1-1-onto→(◡𝑓 “ 𝐴)) |
114 | | f1ofun 6663 |
. . . . . . . . . 10
⊢ ((◡𝑓 ↾ 𝐴):𝐴–1-1-onto→(◡𝑓 “ 𝐴) → Fun (◡𝑓 ↾ 𝐴)) |
115 | 111, 113,
114 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → Fun (◡𝑓 ↾ 𝐴)) |
116 | 104, 108,
115 | 3jca 1130 |
. . . . . . . 8
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
117 | 116 | ex 416 |
. . . . . . 7
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → (𝑓:ℕ–1-1-onto→𝐴 → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
118 | 98, 117 | eximd 2214 |
. . . . . 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 957 |
. . 3
⊢ (((𝐴 ≺ ω ∨ 𝐴 ≈ ω) ∧ 𝑍 ∈ 𝑉) → (¬ 𝑍 ∈ 𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
122 | 121 | 3impia 1119 |
. 2
⊢ (((𝐴 ≺ ω ∨ 𝐴 ≈ ω) ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
123 | 1, 122 | syl3an1b 1405 |
1
⊢ ((𝐴 ≼ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |