Step | Hyp | Ref
| Expression |
1 | | brdom2 7871 |
. 2
⊢ (𝐴 ≼ ω ↔ (𝐴 ≺ ω ∨ 𝐴 ≈
ω)) |
2 | | isfinite2 8103 |
. . . . . . . . . 10
⊢ (𝐴 ≺ ω → 𝐴 ∈ Fin) |
3 | | isfinite4 13014 |
. . . . . . . . . 10
⊢ (𝐴 ∈ Fin ↔
(1...(#‘𝐴)) ≈
𝐴) |
4 | 2, 3 | sylib 207 |
. . . . . . . . 9
⊢ (𝐴 ≺ ω →
(1...(#‘𝐴)) ≈
𝐴) |
5 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) → (1...(#‘𝐴)) ≈ 𝐴) |
6 | | bren 7850 |
. . . . . . . 8
⊢
((1...(#‘𝐴))
≈ 𝐴 ↔
∃𝑔 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) |
7 | 5, 6 | sylib 207 |
. . . . . . 7
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) → ∃𝑔 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) |
8 | 7 | 3adant3 1074 |
. . . . . 6
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑔 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) |
9 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑔(𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) |
10 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑔∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)) |
11 | | f1of 6050 |
. . . . . . . . . . . . 13
⊢ (𝑔:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝑔:(1...(#‘𝐴))⟶𝐴) |
12 | 11 | adantl 481 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → 𝑔:(1...(#‘𝐴))⟶𝐴) |
13 | | fconstmpt 5085 |
. . . . . . . . . . . . . 14
⊢ ((ℕ
∖ (1...(#‘𝐴)))
× {𝑍}) = (𝑥 ∈ (ℕ ∖
(1...(#‘𝐴))) ↦
𝑍) |
14 | 13 | eqcomi 2619 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (ℕ ∖
(1...(#‘𝐴))) ↦
𝑍) = ((ℕ ∖
(1...(#‘𝐴))) ×
{𝑍}) |
15 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → 𝑍 ∈ 𝑉) |
16 | | fconst2g 6373 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ 𝑉 → ((𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍):(ℕ ∖ (1...(#‘𝐴)))⟶{𝑍} ↔ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍) = ((ℕ ∖ (1...(#‘𝐴))) × {𝑍}))) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → ((𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍):(ℕ ∖ (1...(#‘𝐴)))⟶{𝑍} ↔ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍) = ((ℕ ∖ (1...(#‘𝐴))) × {𝑍}))) |
18 | 14, 17 | mpbiri 247 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍):(ℕ ∖ (1...(#‘𝐴)))⟶{𝑍}) |
19 | | disjdif 3992 |
. . . . . . . . . . . . 13
⊢
((1...(#‘𝐴))
∩ (ℕ ∖ (1...(#‘𝐴)))) = ∅ |
20 | 19 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → ((1...(#‘𝐴)) ∩ (ℕ ∖
(1...(#‘𝐴)))) =
∅) |
21 | | fun 5979 |
. . . . . . . . . . . 12
⊢ (((𝑔:(1...(#‘𝐴))⟶𝐴 ∧ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍):(ℕ ∖ (1...(#‘𝐴)))⟶{𝑍}) ∧ ((1...(#‘𝐴)) ∩ (ℕ ∖
(1...(#‘𝐴)))) =
∅) → (𝑔 ∪
(𝑥 ∈ (ℕ ∖
(1...(#‘𝐴))) ↦
𝑍)):((1...(#‘𝐴)) ∪ (ℕ ∖
(1...(#‘𝐴))))⟶(𝐴 ∪ {𝑍})) |
22 | 12, 18, 20, 21 | syl21anc 1317 |
. . . . . . . . . . 11
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)):((1...(#‘𝐴)) ∪ (ℕ ∖
(1...(#‘𝐴))))⟶(𝐴 ∪ {𝑍})) |
23 | | fz1ssnn 12243 |
. . . . . . . . . . . . 13
⊢
(1...(#‘𝐴))
⊆ ℕ |
24 | | undif 4001 |
. . . . . . . . . . . . 13
⊢
((1...(#‘𝐴))
⊆ ℕ ↔ ((1...(#‘𝐴)) ∪ (ℕ ∖
(1...(#‘𝐴)))) =
ℕ) |
25 | 23, 24 | mpbi 219 |
. . . . . . . . . . . 12
⊢
((1...(#‘𝐴))
∪ (ℕ ∖ (1...(#‘𝐴)))) = ℕ |
26 | 25 | feq2i 5950 |
. . . . . . . . . . 11
⊢ ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)):((1...(#‘𝐴)) ∪ (ℕ ∖
(1...(#‘𝐴))))⟶(𝐴 ∪ {𝑍}) ↔ (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍})) |
27 | 22, 26 | sylib 207 |
. . . . . . . . . 10
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍})) |
28 | 27 | 3adantl3 1212 |
. . . . . . . . 9
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍})) |
29 | | ssid 3587 |
. . . . . . . . . . . . . 14
⊢ 𝐴 ⊆ 𝐴 |
30 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) |
31 | | f1ofo 6057 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:(1...(#‘𝐴))–1-1-onto→𝐴 → 𝑔:(1...(#‘𝐴))–onto→𝐴) |
32 | | forn 6031 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:(1...(#‘𝐴))–onto→𝐴 → ran 𝑔 = 𝐴) |
33 | 30, 31, 32 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → ran 𝑔 = 𝐴) |
34 | 29, 33 | syl5sseqr 3617 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ ran 𝑔) |
35 | 34 | orcd 406 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → (𝐴 ⊆ ran 𝑔 ∨ 𝐴 ⊆ ran (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍))) |
36 | | ssun 3754 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ran 𝑔 ∨ 𝐴 ⊆ ran (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) → 𝐴 ⊆ (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍))) |
38 | | rnun 5460 |
. . . . . . . . . . 11
⊢ ran
(𝑔 ∪ (𝑥 ∈ (ℕ ∖
(1...(#‘𝐴))) ↦
𝑍)) = (ran 𝑔 ∪ ran (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) |
39 | 37, 38 | syl6sseqr 3615 |
. . . . . . . . . 10
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍))) |
40 | 39 | 3adantl3 1212 |
. . . . . . . . 9
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍))) |
41 | | dff1o3 6056 |
. . . . . . . . . . . 12
⊢ (𝑔:(1...(#‘𝐴))–1-1-onto→𝐴 ↔ (𝑔:(1...(#‘𝐴))–onto→𝐴 ∧ Fun ◡𝑔)) |
42 | 41 | simprbi 479 |
. . . . . . . . . . 11
⊢ (𝑔:(1...(#‘𝐴))–1-1-onto→𝐴 → Fun ◡𝑔) |
43 | 42 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → Fun ◡𝑔) |
44 | | cnvun 5457 |
. . . . . . . . . . . . . 14
⊢ ◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) = (◡𝑔 ∪ ◡(𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) |
45 | 44 | reseq1i 5313 |
. . . . . . . . . . . . 13
⊢ (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) ↾ 𝐴) = ((◡𝑔 ∪ ◡(𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) ↾ 𝐴) |
46 | | resundir 5331 |
. . . . . . . . . . . . 13
⊢ ((◡𝑔 ∪ ◡(𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) ↾ 𝐴) = ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍) ↾ 𝐴)) |
47 | 45, 46 | eqtri 2632 |
. . . . . . . . . . . 12
⊢ (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) ↾ 𝐴) = ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍) ↾ 𝐴)) |
48 | | dff1o4 6058 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔:(1...(#‘𝐴))–1-1-onto→𝐴 ↔ (𝑔 Fn (1...(#‘𝐴)) ∧ ◡𝑔 Fn 𝐴)) |
49 | 48 | simprbi 479 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔:(1...(#‘𝐴))–1-1-onto→𝐴 → ◡𝑔 Fn 𝐴) |
50 | | fnresdm 5914 |
. . . . . . . . . . . . . . . 16
⊢ (◡𝑔 Fn 𝐴 → (◡𝑔 ↾ 𝐴) = ◡𝑔) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑔:(1...(#‘𝐴))–1-1-onto→𝐴 → (◡𝑔 ↾ 𝐴) = ◡𝑔) |
52 | 51 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → (◡𝑔 ↾ 𝐴) = ◡𝑔) |
53 | | simpl3 1059 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → ¬ 𝑍 ∈ 𝐴) |
54 | 14 | cnveqi 5219 |
. . . . . . . . . . . . . . . . . 18
⊢ ◡(𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍) = ◡((ℕ ∖ (1...(#‘𝐴))) × {𝑍}) |
55 | | cnvxp 5470 |
. . . . . . . . . . . . . . . . . 18
⊢ ◡((ℕ ∖ (1...(#‘𝐴))) × {𝑍}) = ({𝑍} × (ℕ ∖
(1...(#‘𝐴)))) |
56 | 54, 55 | eqtri 2632 |
. . . . . . . . . . . . . . . . 17
⊢ ◡(𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍) = ({𝑍} × (ℕ ∖
(1...(#‘𝐴)))) |
57 | 56 | reseq1i 5313 |
. . . . . . . . . . . . . . . 16
⊢ (◡(𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍) ↾ 𝐴) = (({𝑍} × (ℕ ∖
(1...(#‘𝐴)))) ↾
𝐴) |
58 | | incom 3767 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∩ {𝑍}) = ({𝑍} ∩ 𝐴) |
59 | | disjsn 4192 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∩ {𝑍}) = ∅ ↔ ¬ 𝑍 ∈ 𝐴) |
60 | 59 | biimpri 217 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑍 ∈ 𝐴 → (𝐴 ∩ {𝑍}) = ∅) |
61 | 58, 60 | syl5eqr 2658 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑍 ∈ 𝐴 → ({𝑍} ∩ 𝐴) = ∅) |
62 | | xpdisjres 28793 |
. . . . . . . . . . . . . . . . 17
⊢ (({𝑍} ∩ 𝐴) = ∅ → (({𝑍} × (ℕ ∖
(1...(#‘𝐴)))) ↾
𝐴) =
∅) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑍 ∈ 𝐴 → (({𝑍} × (ℕ ∖
(1...(#‘𝐴)))) ↾
𝐴) =
∅) |
64 | 57, 63 | syl5eq 2656 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑍 ∈ 𝐴 → (◡(𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍) ↾ 𝐴) = ∅) |
65 | 53, 64 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → (◡(𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍) ↾ 𝐴) = ∅) |
66 | 52, 65 | uneq12d 3730 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍) ↾ 𝐴)) = (◡𝑔 ∪ ∅)) |
67 | | un0 3919 |
. . . . . . . . . . . . 13
⊢ (◡𝑔 ∪ ∅) = ◡𝑔 |
68 | 66, 67 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → ((◡𝑔 ↾ 𝐴) ∪ (◡(𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍) ↾ 𝐴)) = ◡𝑔) |
69 | 47, 68 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) ↾ 𝐴) = ◡𝑔) |
70 | 69 | funeqd 5825 |
. . . . . . . . . 10
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → (Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) ↾ 𝐴) ↔ Fun ◡𝑔)) |
71 | 43, 70 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) ↾ 𝐴)) |
72 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑔 ∈ V |
73 | | nnex 10903 |
. . . . . . . . . . . . 13
⊢ ℕ
∈ V |
74 | | difexg 4735 |
. . . . . . . . . . . . 13
⊢ (ℕ
∈ V → (ℕ ∖ (1...(#‘𝐴))) ∈ V) |
75 | 73, 74 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (ℕ
∖ (1...(#‘𝐴)))
∈ V |
76 | 75 | mptex 6390 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (ℕ ∖
(1...(#‘𝐴))) ↦
𝑍) ∈
V |
77 | 72, 76 | unex 6854 |
. . . . . . . . . 10
⊢ (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) ∈ V |
78 | | feq1 5939 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ↔ (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}))) |
79 | | rneq 5272 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) → ran 𝑓 = ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍))) |
80 | 79 | sseq2d 3596 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) → (𝐴 ⊆ ran 𝑓 ↔ 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)))) |
81 | | cnveq 5218 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) → ◡𝑓 = ◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍))) |
82 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) → 𝐴 = 𝐴) |
83 | 81, 82 | reseq12d 5318 |
. . . . . . . . . . . 12
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) → (◡𝑓 ↾ 𝐴) = (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) ↾ 𝐴)) |
84 | 83 | funeqd 5825 |
. . . . . . . . . . 11
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) → (Fun (◡𝑓 ↾ 𝐴) ↔ Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) ↾ 𝐴))) |
85 | 78, 80, 84 | 3anbi123d 1391 |
. . . . . . . . . 10
⊢ (𝑓 = (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) → ((𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)) ↔ ((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) ∧ Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) ↾ 𝐴)))) |
86 | 77, 85 | spcev 3273 |
. . . . . . . . 9
⊢ (((𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)):ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran (𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) ∧ Fun (◡(𝑔 ∪ (𝑥 ∈ (ℕ ∖ (1...(#‘𝐴))) ↦ 𝑍)) ↾ 𝐴)) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
87 | 28, 40, 71, 86 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) ∧ 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
88 | 87 | ex 449 |
. . . . . . 7
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → (𝑔:(1...(#‘𝐴))–1-1-onto→𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
89 | 9, 10, 88 | exlimd 2074 |
. . . . . 6
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → (∃𝑔 𝑔:(1...(#‘𝐴))–1-1-onto→𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
90 | 8, 89 | mpd 15 |
. . . . 5
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
91 | 90 | 3expia 1259 |
. . . 4
⊢ ((𝐴 ≺ ω ∧ 𝑍 ∈ 𝑉) → (¬ 𝑍 ∈ 𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
92 | | nnenom 12641 |
. . . . . . . 8
⊢ ℕ
≈ ω |
93 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → 𝐴 ≈ ω) |
94 | 93 | ensymd 7893 |
. . . . . . . 8
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ω ≈ 𝐴) |
95 | | entr 7894 |
. . . . . . . 8
⊢ ((ℕ
≈ ω ∧ ω ≈ 𝐴) → ℕ ≈ 𝐴) |
96 | 92, 94, 95 | sylancr 694 |
. . . . . . 7
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ℕ ≈ 𝐴) |
97 | | bren 7850 |
. . . . . . 7
⊢ (ℕ
≈ 𝐴 ↔
∃𝑓 𝑓:ℕ–1-1-onto→𝐴) |
98 | 96, 97 | sylib 207 |
. . . . . 6
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ∃𝑓 𝑓:ℕ–1-1-onto→𝐴) |
99 | | nfv 1830 |
. . . . . . 7
⊢
Ⅎ𝑓(𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) |
100 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓:ℕ–1-1-onto→𝐴) |
101 | | f1of 6050 |
. . . . . . . . . 10
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:ℕ⟶𝐴) |
102 | | ssun1 3738 |
. . . . . . . . . . 11
⊢ 𝐴 ⊆ (𝐴 ∪ {𝑍}) |
103 | | fss 5969 |
. . . . . . . . . . 11
⊢ ((𝑓:ℕ⟶𝐴 ∧ 𝐴 ⊆ (𝐴 ∪ {𝑍})) → 𝑓:ℕ⟶(𝐴 ∪ {𝑍})) |
104 | 102, 103 | mpan2 703 |
. . . . . . . . . 10
⊢ (𝑓:ℕ⟶𝐴 → 𝑓:ℕ⟶(𝐴 ∪ {𝑍})) |
105 | 100, 101,
104 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝑓:ℕ⟶(𝐴 ∪ {𝑍})) |
106 | | f1ofo 6057 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–1-1-onto→𝐴 → 𝑓:ℕ–onto→𝐴) |
107 | | forn 6031 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–onto→𝐴 → ran 𝑓 = 𝐴) |
108 | 100, 106,
107 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → ran 𝑓 = 𝐴) |
109 | 29, 108 | syl5sseqr 3617 |
. . . . . . . . 9
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → 𝐴 ⊆ ran 𝑓) |
110 | | f1ocnv 6062 |
. . . . . . . . . . 11
⊢ (𝑓:ℕ–1-1-onto→𝐴 → ◡𝑓:𝐴–1-1-onto→ℕ) |
111 | | f1of1 6049 |
. . . . . . . . . . 11
⊢ (◡𝑓:𝐴–1-1-onto→ℕ → ◡𝑓:𝐴–1-1→ℕ) |
112 | 100, 110,
111 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → ◡𝑓:𝐴–1-1→ℕ) |
113 | | f1ores 6064 |
. . . . . . . . . . 11
⊢ ((◡𝑓:𝐴–1-1→ℕ ∧ 𝐴 ⊆ 𝐴) → (◡𝑓 ↾ 𝐴):𝐴–1-1-onto→(◡𝑓 “ 𝐴)) |
114 | 29, 113 | mpan2 703 |
. . . . . . . . . 10
⊢ (◡𝑓:𝐴–1-1→ℕ → (◡𝑓 ↾ 𝐴):𝐴–1-1-onto→(◡𝑓 “ 𝐴)) |
115 | | f1ofun 6052 |
. . . . . . . . . 10
⊢ ((◡𝑓 ↾ 𝐴):𝐴–1-1-onto→(◡𝑓 “ 𝐴) → Fun (◡𝑓 ↾ 𝐴)) |
116 | 112, 114,
115 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → Fun (◡𝑓 ↾ 𝐴)) |
117 | 105, 109,
116 | 3jca 1235 |
. . . . . . . 8
⊢ (((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) ∧ 𝑓:ℕ–1-1-onto→𝐴) → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
118 | 117 | ex 449 |
. . . . . . 7
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → (𝑓:ℕ–1-1-onto→𝐴 → (𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
119 | 99, 118 | eximd 2072 |
. . . . . 6
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → (∃𝑓 𝑓:ℕ–1-1-onto→𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
120 | 98, 119 | mpd 15 |
. . . . 5
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
121 | 120 | a1d 25 |
. . . 4
⊢ ((𝐴 ≈ ω ∧ 𝑍 ∈ 𝑉) → (¬ 𝑍 ∈ 𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
122 | 91, 121 | jaoian 820 |
. . 3
⊢ (((𝐴 ≺ ω ∨ 𝐴 ≈ ω) ∧ 𝑍 ∈ 𝑉) → (¬ 𝑍 ∈ 𝐴 → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴)))) |
123 | 122 | 3impia 1253 |
. 2
⊢ (((𝐴 ≺ ω ∨ 𝐴 ≈ ω) ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |
124 | 1, 123 | syl3an1b 1354 |
1
⊢ ((𝐴 ≼ ω ∧ 𝑍 ∈ 𝑉 ∧ ¬ 𝑍 ∈ 𝐴) → ∃𝑓(𝑓:ℕ⟶(𝐴 ∪ {𝑍}) ∧ 𝐴 ⊆ ran 𝑓 ∧ Fun (◡𝑓 ↾ 𝐴))) |