Step | Hyp | Ref
| Expression |
1 | | cantnfub.m |
. . . . . . 7
⊢ (𝜑 → 𝑀:𝑁⟶ω) |
2 | 1 | ad2antrr 725 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑥 ∈ ran 𝐴) → 𝑀:𝑁⟶ω) |
3 | | cantnfub.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:𝑁–1-1→𝑋) |
4 | 3 | ad2antrr 725 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑥 ∈ ran 𝐴) → 𝐴:𝑁–1-1→𝑋) |
5 | | f1f1orn 6841 |
. . . . . . . 8
⊢ (𝐴:𝑁–1-1→𝑋 → 𝐴:𝑁–1-1-onto→ran
𝐴) |
6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑥 ∈ ran 𝐴) → 𝐴:𝑁–1-1-onto→ran
𝐴) |
7 | | f1ocnvdm 7278 |
. . . . . . 7
⊢ ((𝐴:𝑁–1-1-onto→ran
𝐴 ∧ 𝑥 ∈ ran 𝐴) → (◡𝐴‘𝑥) ∈ 𝑁) |
8 | 6, 7 | sylancom 589 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑥 ∈ ran 𝐴) → (◡𝐴‘𝑥) ∈ 𝑁) |
9 | 2, 8 | ffvelcdmd 7083 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑥 ∈ ran 𝐴) → (𝑀‘(◡𝐴‘𝑥)) ∈ ω) |
10 | | peano1 7874 |
. . . . . 6
⊢ ∅
∈ ω |
11 | 10 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ 𝑥 ∈ ran 𝐴) → ∅ ∈
ω) |
12 | 9, 11 | ifclda 4562 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → if(𝑥 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑥)), ∅) ∈ ω) |
13 | | cantnfub.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ if(𝑥 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑥)), ∅)) |
14 | 12, 13 | fmptd 7109 |
. . 3
⊢ (𝜑 → 𝐹:𝑋⟶ω) |
15 | | f1fn 6785 |
. . . . . . . 8
⊢ (𝐴:𝑁–1-1→𝑋 → 𝐴 Fn 𝑁) |
16 | 3, 15 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 Fn 𝑁) |
17 | | cantnfub.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ω) |
18 | | nnon 7856 |
. . . . . . . . 9
⊢ (𝑁 ∈ ω → 𝑁 ∈ On) |
19 | | onfin 9226 |
. . . . . . . . 9
⊢ (𝑁 ∈ On → (𝑁 ∈ Fin ↔ 𝑁 ∈
ω)) |
20 | 17, 18, 19 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 ∈ Fin ↔ 𝑁 ∈ ω)) |
21 | 17, 20 | mpbird 257 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ Fin) |
22 | 16, 21 | jca 513 |
. . . . . 6
⊢ (𝜑 → (𝐴 Fn 𝑁 ∧ 𝑁 ∈ Fin)) |
23 | | fnfi 9177 |
. . . . . 6
⊢ ((𝐴 Fn 𝑁 ∧ 𝑁 ∈ Fin) → 𝐴 ∈ Fin) |
24 | | rnfi 9331 |
. . . . . 6
⊢ (𝐴 ∈ Fin → ran 𝐴 ∈ Fin) |
25 | 22, 23, 24 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ran 𝐴 ∈ Fin) |
26 | | eldifi 4125 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑋 ∖ ran 𝐴) → 𝑦 ∈ 𝑋) |
27 | 26 | adantl 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ ran 𝐴)) → 𝑦 ∈ 𝑋) |
28 | | eleq1w 2817 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ∈ ran 𝐴 ↔ 𝑦 ∈ ran 𝐴)) |
29 | | 2fveq3 6893 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑀‘(◡𝐴‘𝑥)) = (𝑀‘(◡𝐴‘𝑦))) |
30 | 28, 29 | ifbieq1d 4551 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → if(𝑥 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑥)), ∅) = if(𝑦 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑦)), ∅)) |
31 | | fvex 6901 |
. . . . . . . . . 10
⊢ (𝑀‘(◡𝐴‘𝑦)) ∈ V |
32 | | 0ex 5306 |
. . . . . . . . . 10
⊢ ∅
∈ V |
33 | 31, 32 | ifex 4577 |
. . . . . . . . 9
⊢ if(𝑦 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑦)), ∅) ∈ V |
34 | 30, 13, 33 | fvmpt 6994 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = if(𝑦 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑦)), ∅)) |
35 | 27, 34 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ ran 𝐴)) → (𝐹‘𝑦) = if(𝑦 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑦)), ∅)) |
36 | | eldifn 4126 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑋 ∖ ran 𝐴) → ¬ 𝑦 ∈ ran 𝐴) |
37 | 36 | adantl 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ ran 𝐴)) → ¬ 𝑦 ∈ ran 𝐴) |
38 | 37 | iffalsed 4538 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ ran 𝐴)) → if(𝑦 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑦)), ∅) = ∅) |
39 | 35, 38 | eqtrd 2773 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ ran 𝐴)) → (𝐹‘𝑦) = ∅) |
40 | 14, 39 | suppss 8174 |
. . . . 5
⊢ (𝜑 → (𝐹 supp ∅) ⊆ ran 𝐴) |
41 | 25, 40 | ssfid 9263 |
. . . 4
⊢ (𝜑 → (𝐹 supp ∅) ∈ Fin) |
42 | 14 | ffund 6718 |
. . . . 5
⊢ (𝜑 → Fun 𝐹) |
43 | | omelon 9637 |
. . . . . . . 8
⊢ ω
∈ On |
44 | 43 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ω ∈
On) |
45 | | cantnfub.0 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ On) |
46 | 44, 45 | elmapd 8830 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∈ (ω ↑m 𝑋) ↔ 𝐹:𝑋⟶ω)) |
47 | 14, 46 | mpbird 257 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (ω ↑m 𝑋)) |
48 | 10 | a1i 11 |
. . . . 5
⊢ (𝜑 → ∅ ∈
ω) |
49 | | funisfsupp 9363 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ (ω ↑m 𝑋) ∧ ∅ ∈ ω)
→ (𝐹 finSupp ∅
↔ (𝐹 supp ∅)
∈ Fin)) |
50 | 42, 47, 48, 49 | syl3anc 1372 |
. . . 4
⊢ (𝜑 → (𝐹 finSupp ∅ ↔ (𝐹 supp ∅) ∈ Fin)) |
51 | 41, 50 | mpbird 257 |
. . 3
⊢ (𝜑 → 𝐹 finSupp ∅) |
52 | | eqid 2733 |
. . . 4
⊢ dom
(ω CNF 𝑋) = dom
(ω CNF 𝑋) |
53 | 52, 44, 45 | cantnfs 9657 |
. . 3
⊢ (𝜑 → (𝐹 ∈ dom (ω CNF 𝑋) ↔ (𝐹:𝑋⟶ω ∧ 𝐹 finSupp ∅))) |
54 | 14, 51, 53 | mpbir2and 712 |
. 2
⊢ (𝜑 → 𝐹 ∈ dom (ω CNF 𝑋)) |
55 | 52, 44, 45 | cantnff 9665 |
. . 3
⊢ (𝜑 → (ω CNF 𝑋):dom (ω CNF 𝑋)⟶(ω
↑o 𝑋)) |
56 | 55, 54 | ffvelcdmd 7083 |
. 2
⊢ (𝜑 → ((ω CNF 𝑋)‘𝐹) ∈ (ω ↑o 𝑋)) |
57 | 54, 56 | jca 513 |
1
⊢ (𝜑 → (𝐹 ∈ dom (ω CNF 𝑋) ∧ ((ω CNF 𝑋)‘𝐹) ∈ (ω ↑o 𝑋))) |