| Step | Hyp | Ref
| Expression |
| 1 | | fvex 6919 |
. . . 4
⊢
(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ) ∈ V |
| 2 | 1 | csbex 5311 |
. . 3
⊢
⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ) ∈ V |
| 3 | 2 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ) ∈ V) |
| 4 | | eqid 2737 |
. . . 4
⊢ {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅} = {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅} |
| 5 | | cantnfs.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ On) |
| 6 | | cantnfs.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ On) |
| 7 | 4, 5, 6 | cantnffval 9703 |
. . 3
⊢ (𝜑 → (𝐴 CNF 𝐵) = (𝑓 ∈ {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅} ↦
⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ))) |
| 8 | | cantnfs.s |
. . . . 5
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
| 9 | 4, 5, 6 | cantnfdm 9704 |
. . . . 5
⊢ (𝜑 → dom (𝐴 CNF 𝐵) = {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅}) |
| 10 | 8, 9 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → 𝑆 = {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅}) |
| 11 | 10 | mpteq1d 5237 |
. . 3
⊢ (𝜑 → (𝑓 ∈ 𝑆 ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ)) = (𝑓 ∈ {𝑔 ∈ (𝐴 ↑m 𝐵) ∣ 𝑔 finSupp ∅} ↦
⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ))) |
| 12 | 7, 11 | eqtr4d 2780 |
. 2
⊢ (𝜑 → (𝐴 CNF 𝐵) = (𝑓 ∈ 𝑆 ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (ℎ‘𝑘)) ·o (𝑓‘(ℎ‘𝑘))) +o 𝑧)), ∅)‘dom ℎ))) |
| 13 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ On) |
| 14 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ On) |
| 15 | | eqid 2737 |
. . . . . . . 8
⊢ OrdIso( E
, (𝑥 supp ∅)) =
OrdIso( E , (𝑥 supp
∅)) |
| 16 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
| 17 | | eqid 2737 |
. . . . . . . 8
⊢
seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (OrdIso( E , (𝑥 supp ∅))‘𝑘)) ·o (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +o 𝑧)), ∅) =
seqω((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑o (OrdIso( E , (𝑥 supp ∅))‘𝑘)) ·o (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +o 𝑧)), ∅) |
| 18 | 8, 13, 14, 15, 16, 17 | cantnfval 9708 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝐴 CNF 𝐵)‘𝑥) = (seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (OrdIso( E , (𝑥 supp ∅))‘𝑘)) ·o (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +o 𝑧)), ∅)‘dom OrdIso( E
, (𝑥 supp
∅)))) |
| 19 | 18 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → ((𝐴 CNF 𝐵)‘𝑥) = (seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (OrdIso( E , (𝑥 supp ∅))‘𝑘)) ·o (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +o 𝑧)), ∅)‘dom OrdIso( E
, (𝑥 supp
∅)))) |
| 20 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝑥 supp ∅) ∈
V |
| 21 | 8, 13, 14, 15, 16 | cantnfcl 9707 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ( E We (𝑥 supp ∅) ∧ dom OrdIso( E , (𝑥 supp ∅)) ∈
ω)) |
| 22 | 21 | simpld 494 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → E We (𝑥 supp ∅)) |
| 23 | 15 | oien 9578 |
. . . . . . . . . . 11
⊢ (((𝑥 supp ∅) ∈ V ∧ E
We (𝑥 supp ∅)) →
dom OrdIso( E , (𝑥 supp
∅)) ≈ (𝑥 supp
∅)) |
| 24 | 20, 22, 23 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → dom OrdIso( E , (𝑥 supp ∅)) ≈ (𝑥 supp ∅)) |
| 25 | 24 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → dom OrdIso( E , (𝑥 supp ∅)) ≈ (𝑥 supp ∅)) |
| 26 | | suppssdm 8202 |
. . . . . . . . . . 11
⊢ (𝑥 supp ∅) ⊆ dom 𝑥 |
| 27 | 8, 5, 6 | cantnfs 9706 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↔ (𝑥:𝐵⟶𝐴 ∧ 𝑥 finSupp ∅))) |
| 28 | 27 | simprbda 498 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥:𝐵⟶𝐴) |
| 29 | 26, 28 | fssdm 6755 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 supp ∅) ⊆ 𝐵) |
| 30 | | feq3 6718 |
. . . . . . . . . . . . . 14
⊢ (𝐴 = ∅ → (𝑥:𝐵⟶𝐴 ↔ 𝑥:𝐵⟶∅)) |
| 31 | 28, 30 | syl5ibcom 245 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐴 = ∅ → 𝑥:𝐵⟶∅)) |
| 32 | 31 | imp 406 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → 𝑥:𝐵⟶∅) |
| 33 | | f00 6790 |
. . . . . . . . . . . 12
⊢ (𝑥:𝐵⟶∅ ↔ (𝑥 = ∅ ∧ 𝐵 = ∅)) |
| 34 | 32, 33 | sylib 218 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → (𝑥 = ∅ ∧ 𝐵 = ∅)) |
| 35 | 34 | simprd 495 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → 𝐵 = ∅) |
| 36 | | sseq0 4403 |
. . . . . . . . . 10
⊢ (((𝑥 supp ∅) ⊆ 𝐵 ∧ 𝐵 = ∅) → (𝑥 supp ∅) = ∅) |
| 37 | 29, 35, 36 | syl2an2r 685 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → (𝑥 supp ∅) = ∅) |
| 38 | 25, 37 | breqtrd 5169 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → dom OrdIso( E , (𝑥 supp ∅)) ≈
∅) |
| 39 | | en0 9058 |
. . . . . . . 8
⊢ (dom
OrdIso( E , (𝑥 supp
∅)) ≈ ∅ ↔ dom OrdIso( E , (𝑥 supp ∅)) = ∅) |
| 40 | 38, 39 | sylib 218 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → dom OrdIso( E , (𝑥 supp ∅)) =
∅) |
| 41 | 40 | fveq2d 6910 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) →
(seqω((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑o (OrdIso( E , (𝑥 supp ∅))‘𝑘)) ·o (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +o 𝑧)), ∅)‘dom OrdIso( E , (𝑥 supp ∅))) =
(seqω((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑o (OrdIso( E , (𝑥 supp ∅))‘𝑘)) ·o (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +o 𝑧)), ∅)‘∅)) |
| 42 | | 0ex 5307 |
. . . . . . 7
⊢ ∅
∈ V |
| 43 | 17 | seqom0g 8496 |
. . . . . . 7
⊢ (∅
∈ V → (seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (OrdIso( E , (𝑥 supp ∅))‘𝑘)) ·o (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +o 𝑧)), ∅)‘∅) =
∅) |
| 44 | 42, 43 | mp1i 13 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) →
(seqω((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑o (OrdIso( E , (𝑥 supp ∅))‘𝑘)) ·o (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +o 𝑧)), ∅)‘∅) =
∅) |
| 45 | 19, 41, 44 | 3eqtrd 2781 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → ((𝐴 CNF 𝐵)‘𝑥) = ∅) |
| 46 | | el1o 8533 |
. . . . 5
⊢ (((𝐴 CNF 𝐵)‘𝑥) ∈ 1o ↔ ((𝐴 CNF 𝐵)‘𝑥) = ∅) |
| 47 | 45, 46 | sylibr 234 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → ((𝐴 CNF 𝐵)‘𝑥) ∈ 1o) |
| 48 | 35 | oveq2d 7447 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → (𝐴 ↑o 𝐵) = (𝐴 ↑o
∅)) |
| 49 | 13 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → 𝐴 ∈ On) |
| 50 | | oe0 8560 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝐴 ↑o ∅) =
1o) |
| 51 | 49, 50 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → (𝐴 ↑o ∅) =
1o) |
| 52 | 48, 51 | eqtrd 2777 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → (𝐴 ↑o 𝐵) = 1o) |
| 53 | 47, 52 | eleqtrrd 2844 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → ((𝐴 CNF 𝐵)‘𝑥) ∈ (𝐴 ↑o 𝐵)) |
| 54 | 13 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 ≠ ∅) → 𝐴 ∈ On) |
| 55 | 14 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 ≠ ∅) → 𝐵 ∈ On) |
| 56 | 16 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 ≠ ∅) → 𝑥 ∈ 𝑆) |
| 57 | | on0eln0 6440 |
. . . . . 6
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 58 | 13, 57 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 59 | 58 | biimpar 477 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴) |
| 60 | 29 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 ≠ ∅) → (𝑥 supp ∅) ⊆ 𝐵) |
| 61 | 8, 54, 55, 56, 59, 55, 60 | cantnflt2 9713 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 ≠ ∅) → ((𝐴 CNF 𝐵)‘𝑥) ∈ (𝐴 ↑o 𝐵)) |
| 62 | 53, 61 | pm2.61dane 3029 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝐴 CNF 𝐵)‘𝑥) ∈ (𝐴 ↑o 𝐵)) |
| 63 | 3, 12, 62 | fmpt2d 7144 |
1
⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑o 𝐵)) |