| Step | Hyp | Ref
| Expression |
| 1 | | cantnfub.m |
. . . . . . 7
⊢ (𝜑 → 𝑀:𝑁⟶ω) |
| 2 | 1 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑥 ∈ ran 𝐴) → 𝑀:𝑁⟶ω) |
| 3 | | cantnfub.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴:𝑁–1-1→𝑋) |
| 4 | 3 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑥 ∈ ran 𝐴) → 𝐴:𝑁–1-1→𝑋) |
| 5 | | f1f1orn 6859 |
. . . . . . . 8
⊢ (𝐴:𝑁–1-1→𝑋 → 𝐴:𝑁–1-1-onto→ran
𝐴) |
| 6 | 4, 5 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑥 ∈ ran 𝐴) → 𝐴:𝑁–1-1-onto→ran
𝐴) |
| 7 | | f1ocnvdm 7305 |
. . . . . . 7
⊢ ((𝐴:𝑁–1-1-onto→ran
𝐴 ∧ 𝑥 ∈ ran 𝐴) → (◡𝐴‘𝑥) ∈ 𝑁) |
| 8 | 6, 7 | sylancom 588 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑥 ∈ ran 𝐴) → (◡𝐴‘𝑥) ∈ 𝑁) |
| 9 | 2, 8 | ffvelcdmd 7105 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ 𝑥 ∈ ran 𝐴) → (𝑀‘(◡𝐴‘𝑥)) ∈ ω) |
| 10 | | peano1 7910 |
. . . . . 6
⊢ ∅
∈ ω |
| 11 | 10 | a1i 11 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑋) ∧ ¬ 𝑥 ∈ ran 𝐴) → ∅ ∈
ω) |
| 12 | 9, 11 | ifclda 4561 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → if(𝑥 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑥)), ∅) ∈ ω) |
| 13 | | cantnfub.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ if(𝑥 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑥)), ∅)) |
| 14 | 12, 13 | fmptd 7134 |
. . 3
⊢ (𝜑 → 𝐹:𝑋⟶ω) |
| 15 | | f1fn 6805 |
. . . . . . . 8
⊢ (𝐴:𝑁–1-1→𝑋 → 𝐴 Fn 𝑁) |
| 16 | 3, 15 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 Fn 𝑁) |
| 17 | | cantnfub.n |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ω) |
| 18 | | nnon 7893 |
. . . . . . . . 9
⊢ (𝑁 ∈ ω → 𝑁 ∈ On) |
| 19 | | onfin 9267 |
. . . . . . . . 9
⊢ (𝑁 ∈ On → (𝑁 ∈ Fin ↔ 𝑁 ∈
ω)) |
| 20 | 17, 18, 19 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 ∈ Fin ↔ 𝑁 ∈ ω)) |
| 21 | 17, 20 | mpbird 257 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ Fin) |
| 22 | 16, 21 | jca 511 |
. . . . . 6
⊢ (𝜑 → (𝐴 Fn 𝑁 ∧ 𝑁 ∈ Fin)) |
| 23 | | fnfi 9218 |
. . . . . 6
⊢ ((𝐴 Fn 𝑁 ∧ 𝑁 ∈ Fin) → 𝐴 ∈ Fin) |
| 24 | | rnfi 9380 |
. . . . . 6
⊢ (𝐴 ∈ Fin → ran 𝐴 ∈ Fin) |
| 25 | 22, 23, 24 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ran 𝐴 ∈ Fin) |
| 26 | | eldifi 4131 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑋 ∖ ran 𝐴) → 𝑦 ∈ 𝑋) |
| 27 | 26 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ ran 𝐴)) → 𝑦 ∈ 𝑋) |
| 28 | | eleq1w 2824 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 ∈ ran 𝐴 ↔ 𝑦 ∈ ran 𝐴)) |
| 29 | | 2fveq3 6911 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑀‘(◡𝐴‘𝑥)) = (𝑀‘(◡𝐴‘𝑦))) |
| 30 | 28, 29 | ifbieq1d 4550 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → if(𝑥 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑥)), ∅) = if(𝑦 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑦)), ∅)) |
| 31 | | fvex 6919 |
. . . . . . . . . 10
⊢ (𝑀‘(◡𝐴‘𝑦)) ∈ V |
| 32 | | 0ex 5307 |
. . . . . . . . . 10
⊢ ∅
∈ V |
| 33 | 31, 32 | ifex 4576 |
. . . . . . . . 9
⊢ if(𝑦 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑦)), ∅) ∈ V |
| 34 | 30, 13, 33 | fvmpt 7016 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝑋 → (𝐹‘𝑦) = if(𝑦 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑦)), ∅)) |
| 35 | 27, 34 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ ran 𝐴)) → (𝐹‘𝑦) = if(𝑦 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑦)), ∅)) |
| 36 | | eldifn 4132 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑋 ∖ ran 𝐴) → ¬ 𝑦 ∈ ran 𝐴) |
| 37 | 36 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ ran 𝐴)) → ¬ 𝑦 ∈ ran 𝐴) |
| 38 | 37 | iffalsed 4536 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ ran 𝐴)) → if(𝑦 ∈ ran 𝐴, (𝑀‘(◡𝐴‘𝑦)), ∅) = ∅) |
| 39 | 35, 38 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑋 ∖ ran 𝐴)) → (𝐹‘𝑦) = ∅) |
| 40 | 14, 39 | suppss 8219 |
. . . . 5
⊢ (𝜑 → (𝐹 supp ∅) ⊆ ran 𝐴) |
| 41 | 25, 40 | ssfid 9301 |
. . . 4
⊢ (𝜑 → (𝐹 supp ∅) ∈ Fin) |
| 42 | 14 | ffund 6740 |
. . . . 5
⊢ (𝜑 → Fun 𝐹) |
| 43 | | omelon 9686 |
. . . . . . . 8
⊢ ω
∈ On |
| 44 | 43 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ω ∈
On) |
| 45 | | cantnfub.0 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ On) |
| 46 | 44, 45 | elmapd 8880 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∈ (ω ↑m 𝑋) ↔ 𝐹:𝑋⟶ω)) |
| 47 | 14, 46 | mpbird 257 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (ω ↑m 𝑋)) |
| 48 | 10 | a1i 11 |
. . . . 5
⊢ (𝜑 → ∅ ∈
ω) |
| 49 | | funisfsupp 9407 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝐹 ∈ (ω ↑m 𝑋) ∧ ∅ ∈ ω)
→ (𝐹 finSupp ∅
↔ (𝐹 supp ∅)
∈ Fin)) |
| 50 | 42, 47, 48, 49 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → (𝐹 finSupp ∅ ↔ (𝐹 supp ∅) ∈ Fin)) |
| 51 | 41, 50 | mpbird 257 |
. . 3
⊢ (𝜑 → 𝐹 finSupp ∅) |
| 52 | | eqid 2737 |
. . . 4
⊢ dom
(ω CNF 𝑋) = dom
(ω CNF 𝑋) |
| 53 | 52, 44, 45 | cantnfs 9706 |
. . 3
⊢ (𝜑 → (𝐹 ∈ dom (ω CNF 𝑋) ↔ (𝐹:𝑋⟶ω ∧ 𝐹 finSupp ∅))) |
| 54 | 14, 51, 53 | mpbir2and 713 |
. 2
⊢ (𝜑 → 𝐹 ∈ dom (ω CNF 𝑋)) |
| 55 | 52, 44, 45 | cantnff 9714 |
. . 3
⊢ (𝜑 → (ω CNF 𝑋):dom (ω CNF 𝑋)⟶(ω
↑o 𝑋)) |
| 56 | 55, 54 | ffvelcdmd 7105 |
. 2
⊢ (𝜑 → ((ω CNF 𝑋)‘𝐹) ∈ (ω ↑o 𝑋)) |
| 57 | 54, 56 | jca 511 |
1
⊢ (𝜑 → (𝐹 ∈ dom (ω CNF 𝑋) ∧ ((ω CNF 𝑋)‘𝐹) ∈ (ω ↑o 𝑋))) |