Step | Hyp | Ref
| Expression |
1 | | fvex 6201 |
. . . 4
⊢
(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ) ∈ V |
2 | 1 | csbex 4793 |
. . 3
⊢
⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ) ∈ V |
3 | 2 | a1i 11 |
. 2
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑆) → ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ) ∈ V) |
4 | | eqid 2622 |
. . . 4
⊢ {𝑔 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑔 finSupp ∅} = {𝑔 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑔 finSupp ∅} |
5 | | cantnfs.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ On) |
6 | | cantnfs.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ On) |
7 | 4, 5, 6 | cantnffval 8560 |
. . 3
⊢ (𝜑 → (𝐴 CNF 𝐵) = (𝑓 ∈ {𝑔 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑔 finSupp ∅} ↦
⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ))) |
8 | | cantnfs.s |
. . . . 5
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
9 | 4, 5, 6 | cantnfdm 8561 |
. . . . 5
⊢ (𝜑 → dom (𝐴 CNF 𝐵) = {𝑔 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑔 finSupp ∅}) |
10 | 8, 9 | syl5eq 2668 |
. . . 4
⊢ (𝜑 → 𝑆 = {𝑔 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑔 finSupp ∅}) |
11 | 10 | mpteq1d 4738 |
. . 3
⊢ (𝜑 → (𝑓 ∈ 𝑆 ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ)) = (𝑓 ∈ {𝑔 ∈ (𝐴 ↑𝑚 𝐵) ∣ 𝑔 finSupp ∅} ↦
⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ))) |
12 | 7, 11 | eqtr4d 2659 |
. 2
⊢ (𝜑 → (𝐴 CNF 𝐵) = (𝑓 ∈ 𝑆 ↦ ⦋OrdIso( E , (𝑓 supp ∅)) / ℎ⦌(seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (ℎ‘𝑘)) ·𝑜 (𝑓‘(ℎ‘𝑘))) +𝑜 𝑧)), ∅)‘dom ℎ))) |
13 | 5 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ On) |
14 | 6 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ On) |
15 | | eqid 2622 |
. . . . . . . 8
⊢ OrdIso( E
, (𝑥 supp ∅)) =
OrdIso( E , (𝑥 supp
∅)) |
16 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
17 | | eqid 2622 |
. . . . . . . 8
⊢
seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
(𝑥 supp
∅))‘𝑘))
·𝑜 (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
(𝑥 supp
∅))‘𝑘))
·𝑜 (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) |
18 | 8, 13, 14, 15, 16, 17 | cantnfval 8565 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝐴 CNF 𝐵)‘𝑥) = (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
(𝑥 supp
∅))‘𝑘))
·𝑜 (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , (𝑥 supp
∅)))) |
19 | 18 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → ((𝐴 CNF 𝐵)‘𝑥) = (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
(𝑥 supp
∅))‘𝑘))
·𝑜 (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , (𝑥 supp
∅)))) |
20 | | ovex 6678 |
. . . . . . . . . . 11
⊢ (𝑥 supp ∅) ∈
V |
21 | 8, 13, 14, 15, 16 | cantnfcl 8564 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ( E We (𝑥 supp ∅) ∧ dom OrdIso( E , (𝑥 supp ∅)) ∈
ω)) |
22 | 21 | simpld 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → E We (𝑥 supp ∅)) |
23 | 15 | oien 8443 |
. . . . . . . . . . 11
⊢ (((𝑥 supp ∅) ∈ V ∧ E
We (𝑥 supp ∅)) →
dom OrdIso( E , (𝑥 supp
∅)) ≈ (𝑥 supp
∅)) |
24 | 20, 22, 23 | sylancr 695 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → dom OrdIso( E , (𝑥 supp ∅)) ≈ (𝑥 supp ∅)) |
25 | 24 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → dom OrdIso( E , (𝑥 supp ∅)) ≈ (𝑥 supp ∅)) |
26 | | suppssdm 7308 |
. . . . . . . . . . 11
⊢ (𝑥 supp ∅) ⊆ dom 𝑥 |
27 | 8, 5, 6 | cantnfs 8563 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝑆 ↔ (𝑥:𝐵⟶𝐴 ∧ 𝑥 finSupp ∅))) |
28 | 27 | simprbda 653 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥:𝐵⟶𝐴) |
29 | | fdm 6051 |
. . . . . . . . . . . 12
⊢ (𝑥:𝐵⟶𝐴 → dom 𝑥 = 𝐵) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → dom 𝑥 = 𝐵) |
31 | 26, 30 | syl5sseq 3653 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑥 supp ∅) ⊆ 𝐵) |
32 | | feq3 6028 |
. . . . . . . . . . . . . 14
⊢ (𝐴 = ∅ → (𝑥:𝐵⟶𝐴 ↔ 𝑥:𝐵⟶∅)) |
33 | 28, 32 | syl5ibcom 235 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐴 = ∅ → 𝑥:𝐵⟶∅)) |
34 | 33 | imp 445 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → 𝑥:𝐵⟶∅) |
35 | | f00 6087 |
. . . . . . . . . . . 12
⊢ (𝑥:𝐵⟶∅ ↔ (𝑥 = ∅ ∧ 𝐵 = ∅)) |
36 | 34, 35 | sylib 208 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → (𝑥 = ∅ ∧ 𝐵 = ∅)) |
37 | 36 | simprd 479 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → 𝐵 = ∅) |
38 | | sseq0 3975 |
. . . . . . . . . 10
⊢ (((𝑥 supp ∅) ⊆ 𝐵 ∧ 𝐵 = ∅) → (𝑥 supp ∅) = ∅) |
39 | 31, 37, 38 | syl2an2r 876 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → (𝑥 supp ∅) = ∅) |
40 | 25, 39 | breqtrd 4679 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → dom OrdIso( E , (𝑥 supp ∅)) ≈
∅) |
41 | | en0 8019 |
. . . . . . . 8
⊢ (dom
OrdIso( E , (𝑥 supp
∅)) ≈ ∅ ↔ dom OrdIso( E , (𝑥 supp ∅)) = ∅) |
42 | 40, 41 | sylib 208 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → dom OrdIso( E , (𝑥 supp ∅)) =
∅) |
43 | 42 | fveq2d 6195 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) →
(seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑𝑜 (OrdIso( E , (𝑥 supp ∅))‘𝑘)) ·𝑜 (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E
, (𝑥 supp ∅))) =
(seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑𝑜 (OrdIso( E , (𝑥 supp ∅))‘𝑘)) ·𝑜 (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +𝑜 𝑧)),
∅)‘∅)) |
44 | | 0ex 4790 |
. . . . . . 7
⊢ ∅
∈ V |
45 | 17 | seqom0g 7551 |
. . . . . . 7
⊢ (∅
∈ V → (seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
(𝑥 supp
∅))‘𝑘))
·𝑜 (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅)‘∅) =
∅) |
46 | 44, 45 | mp1i 13 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) →
(seq𝜔((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑𝑜 (OrdIso( E , (𝑥 supp ∅))‘𝑘)) ·𝑜 (𝑥‘(OrdIso( E , (𝑥 supp ∅))‘𝑘))) +𝑜 𝑧)), ∅)‘∅) =
∅) |
47 | 19, 43, 46 | 3eqtrd 2660 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → ((𝐴 CNF 𝐵)‘𝑥) = ∅) |
48 | | el1o 7579 |
. . . . 5
⊢ (((𝐴 CNF 𝐵)‘𝑥) ∈ 1𝑜 ↔ ((𝐴 CNF 𝐵)‘𝑥) = ∅) |
49 | 47, 48 | sylibr 224 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → ((𝐴 CNF 𝐵)‘𝑥) ∈
1𝑜) |
50 | 37 | oveq2d 6666 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → (𝐴 ↑𝑜 𝐵) = (𝐴 ↑𝑜
∅)) |
51 | 13 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → 𝐴 ∈ On) |
52 | | oe0 7602 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝐴 ↑𝑜
∅) = 1𝑜) |
53 | 51, 52 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → (𝐴 ↑𝑜 ∅) =
1𝑜) |
54 | 50, 53 | eqtrd 2656 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → (𝐴 ↑𝑜 𝐵) =
1𝑜) |
55 | 49, 54 | eleqtrrd 2704 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 = ∅) → ((𝐴 CNF 𝐵)‘𝑥) ∈ (𝐴 ↑𝑜 𝐵)) |
56 | 13 | adantr 481 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 ≠ ∅) → 𝐴 ∈ On) |
57 | 14 | adantr 481 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 ≠ ∅) → 𝐵 ∈ On) |
58 | 16 | adantr 481 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 ≠ ∅) → 𝑥 ∈ 𝑆) |
59 | | on0eln0 5780 |
. . . . . 6
⊢ (𝐴 ∈ On → (∅
∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
60 | 13, 59 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅)) |
61 | 60 | biimpar 502 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 ≠ ∅) → ∅ ∈ 𝐴) |
62 | 31 | adantr 481 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 ≠ ∅) → (𝑥 supp ∅) ⊆ 𝐵) |
63 | 8, 56, 57, 58, 61, 57, 62 | cantnflt2 8570 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝐴 ≠ ∅) → ((𝐴 CNF 𝐵)‘𝑥) ∈ (𝐴 ↑𝑜 𝐵)) |
64 | 55, 63 | pm2.61dane 2881 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝐴 CNF 𝐵)‘𝑥) ∈ (𝐴 ↑𝑜 𝐵)) |
65 | 3, 12, 64 | fmpt2d 6393 |
1
⊢ (𝜑 → (𝐴 CNF 𝐵):𝑆⟶(𝐴 ↑𝑜 𝐵)) |