Step | Hyp | Ref
| Expression |
1 | | cantnfs.s |
. . 3
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
2 | | cantnfs.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ On) |
3 | | cantnfs.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ On) |
4 | | cantnfcl.g |
. . 3
⊢ 𝐺 = OrdIso( E , (𝐹 supp ∅)) |
5 | | cantnfcl.f |
. . 3
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
6 | | cantnfval.h |
. . 3
⊢ 𝐻 = seqω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅) |
7 | 1, 2, 3, 4, 5, 6 | cantnfval 9288 |
. 2
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (𝐻‘dom 𝐺)) |
8 | | ssid 3928 |
. . 3
⊢ dom 𝐺 ⊆ dom 𝐺 |
9 | 1, 2, 3, 4, 5 | cantnfcl 9287 |
. . . . 5
⊢ (𝜑 → ( E We (𝐹 supp ∅) ∧ dom 𝐺 ∈ ω)) |
10 | 9 | simprd 499 |
. . . 4
⊢ (𝜑 → dom 𝐺 ∈ ω) |
11 | | sseq1 3931 |
. . . . . . 7
⊢ (𝑢 = ∅ → (𝑢 ⊆ dom 𝐺 ↔ ∅ ⊆ dom 𝐺)) |
12 | | fveq2 6722 |
. . . . . . . . 9
⊢ (𝑢 = ∅ → (𝐻‘𝑢) = (𝐻‘∅)) |
13 | | 0ex 5205 |
. . . . . . . . . 10
⊢ ∅
∈ V |
14 | 6 | seqom0g 8197 |
. . . . . . . . . 10
⊢ (∅
∈ V → (𝐻‘∅) = ∅) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝐻‘∅) =
∅ |
16 | 12, 15 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝑢 = ∅ → (𝐻‘𝑢) = ∅) |
17 | | fveq2 6722 |
. . . . . . . . 9
⊢ (𝑢 = ∅ →
(seqω((𝑘
∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘∅)) |
18 | | eqid 2737 |
. . . . . . . . . . 11
⊢
seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅) = seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅) |
19 | 18 | seqom0g 8197 |
. . . . . . . . . 10
⊢ (∅
∈ V → (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘∅) =
∅) |
20 | 13, 19 | ax-mp 5 |
. . . . . . . . 9
⊢
(seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘∅) =
∅ |
21 | 17, 20 | eqtrdi 2794 |
. . . . . . . 8
⊢ (𝑢 = ∅ →
(seqω((𝑘
∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢) = ∅) |
22 | 16, 21 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑢 = ∅ → ((𝐻‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢) ↔ ∅ = ∅)) |
23 | 11, 22 | imbi12d 348 |
. . . . . 6
⊢ (𝑢 = ∅ → ((𝑢 ⊆ dom 𝐺 → (𝐻‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢)) ↔ (∅ ⊆ dom 𝐺 → ∅ =
∅))) |
24 | 23 | imbi2d 344 |
. . . . 5
⊢ (𝑢 = ∅ → ((𝜑 → (𝑢 ⊆ dom 𝐺 → (𝐻‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢))) ↔ (𝜑 → (∅ ⊆ dom 𝐺 → ∅ =
∅)))) |
25 | | sseq1 3931 |
. . . . . . 7
⊢ (𝑢 = 𝑣 → (𝑢 ⊆ dom 𝐺 ↔ 𝑣 ⊆ dom 𝐺)) |
26 | | fveq2 6722 |
. . . . . . . 8
⊢ (𝑢 = 𝑣 → (𝐻‘𝑢) = (𝐻‘𝑣)) |
27 | | fveq2 6722 |
. . . . . . . 8
⊢ (𝑢 = 𝑣 → (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣)) |
28 | 26, 27 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑢 = 𝑣 → ((𝐻‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢) ↔ (𝐻‘𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣))) |
29 | 25, 28 | imbi12d 348 |
. . . . . 6
⊢ (𝑢 = 𝑣 → ((𝑢 ⊆ dom 𝐺 → (𝐻‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢)) ↔ (𝑣 ⊆ dom 𝐺 → (𝐻‘𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣)))) |
30 | 29 | imbi2d 344 |
. . . . 5
⊢ (𝑢 = 𝑣 → ((𝜑 → (𝑢 ⊆ dom 𝐺 → (𝐻‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢))) ↔ (𝜑 → (𝑣 ⊆ dom 𝐺 → (𝐻‘𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣))))) |
31 | | sseq1 3931 |
. . . . . . 7
⊢ (𝑢 = suc 𝑣 → (𝑢 ⊆ dom 𝐺 ↔ suc 𝑣 ⊆ dom 𝐺)) |
32 | | fveq2 6722 |
. . . . . . . 8
⊢ (𝑢 = suc 𝑣 → (𝐻‘𝑢) = (𝐻‘suc 𝑣)) |
33 | | fveq2 6722 |
. . . . . . . 8
⊢ (𝑢 = suc 𝑣 → (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘suc 𝑣)) |
34 | 32, 33 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑢 = suc 𝑣 → ((𝐻‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢) ↔ (𝐻‘suc 𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘suc 𝑣))) |
35 | 31, 34 | imbi12d 348 |
. . . . . 6
⊢ (𝑢 = suc 𝑣 → ((𝑢 ⊆ dom 𝐺 → (𝐻‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢)) ↔ (suc 𝑣 ⊆ dom 𝐺 → (𝐻‘suc 𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘suc 𝑣)))) |
36 | 35 | imbi2d 344 |
. . . . 5
⊢ (𝑢 = suc 𝑣 → ((𝜑 → (𝑢 ⊆ dom 𝐺 → (𝐻‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢))) ↔ (𝜑 → (suc 𝑣 ⊆ dom 𝐺 → (𝐻‘suc 𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘suc 𝑣))))) |
37 | | sseq1 3931 |
. . . . . . 7
⊢ (𝑢 = dom 𝐺 → (𝑢 ⊆ dom 𝐺 ↔ dom 𝐺 ⊆ dom 𝐺)) |
38 | | fveq2 6722 |
. . . . . . . 8
⊢ (𝑢 = dom 𝐺 → (𝐻‘𝑢) = (𝐻‘dom 𝐺)) |
39 | | fveq2 6722 |
. . . . . . . 8
⊢ (𝑢 = dom 𝐺 → (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘dom 𝐺)) |
40 | 38, 39 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝑢 = dom 𝐺 → ((𝐻‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢) ↔ (𝐻‘dom 𝐺) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘dom 𝐺))) |
41 | 37, 40 | imbi12d 348 |
. . . . . 6
⊢ (𝑢 = dom 𝐺 → ((𝑢 ⊆ dom 𝐺 → (𝐻‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢)) ↔ (dom 𝐺 ⊆ dom 𝐺 → (𝐻‘dom 𝐺) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘dom 𝐺)))) |
42 | 41 | imbi2d 344 |
. . . . 5
⊢ (𝑢 = dom 𝐺 → ((𝜑 → (𝑢 ⊆ dom 𝐺 → (𝐻‘𝑢) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑢))) ↔ (𝜑 → (dom 𝐺 ⊆ dom 𝐺 → (𝐻‘dom 𝐺) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘dom 𝐺))))) |
43 | | eqid 2737 |
. . . . . 6
⊢ ∅ =
∅ |
44 | 43 | 2a1i 12 |
. . . . 5
⊢ (𝜑 → (∅ ⊆ dom 𝐺 → ∅ =
∅)) |
45 | | sssucid 6295 |
. . . . . . . . . 10
⊢ 𝑣 ⊆ suc 𝑣 |
46 | | sstr 3914 |
. . . . . . . . . 10
⊢ ((𝑣 ⊆ suc 𝑣 ∧ suc 𝑣 ⊆ dom 𝐺) → 𝑣 ⊆ dom 𝐺) |
47 | 45, 46 | mpan 690 |
. . . . . . . . 9
⊢ (suc
𝑣 ⊆ dom 𝐺 → 𝑣 ⊆ dom 𝐺) |
48 | 47 | imim1i 63 |
. . . . . . . 8
⊢ ((𝑣 ⊆ dom 𝐺 → (𝐻‘𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣)) → (suc 𝑣 ⊆ dom 𝐺 → (𝐻‘𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣))) |
49 | | oveq2 7226 |
. . . . . . . . . . 11
⊢ ((𝐻‘𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣) → (𝑣(𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))(𝐻‘𝑣)) = (𝑣(𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))(seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣))) |
50 | 6 | seqomsuc 8198 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ ω → (𝐻‘suc 𝑣) = (𝑣(𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))(𝐻‘𝑣))) |
51 | 50 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺)) → (𝐻‘suc 𝑣) = (𝑣(𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))(𝐻‘𝑣))) |
52 | 18 | seqomsuc 8198 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ ω →
(seqω((𝑘
∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘suc 𝑣) = (𝑣(𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))(seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣))) |
53 | 52 | ad2antrl 728 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺)) → (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘suc 𝑣) = (𝑣(𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))(seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣))) |
54 | | ssv 3930 |
. . . . . . . . . . . . . . . 16
⊢ dom 𝐺 ⊆ V |
55 | | ssv 3930 |
. . . . . . . . . . . . . . . 16
⊢ On
⊆ V |
56 | | resmpo 7335 |
. . . . . . . . . . . . . . . 16
⊢ ((dom
𝐺 ⊆ V ∧ On
⊆ V) → ((𝑘
∈ V, 𝑧 ∈ V
↦ (((𝐴
↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)) ↾ (dom 𝐺 × On)) = (𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))) |
57 | 54, 55, 56 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)) ↾ (dom 𝐺 × On)) = (𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)) |
58 | 57 | oveqi 7231 |
. . . . . . . . . . . . . 14
⊢ (𝑣((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)) ↾ (dom 𝐺 × On))(seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣)) = (𝑣(𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))(seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣)) |
59 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺)) → suc 𝑣 ⊆ dom 𝐺) |
60 | | vex 3417 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑣 ∈ V |
61 | 60 | sucid 6297 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑣 ∈ suc 𝑣 |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺)) → 𝑣 ∈ suc 𝑣) |
63 | 59, 62 | sseldd 3907 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺)) → 𝑣 ∈ dom 𝐺) |
64 | 18 | cantnfvalf 9285 |
. . . . . . . . . . . . . . . . 17
⊢
seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)),
∅):ω⟶On |
65 | 64 | ffvelrni 6908 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ ω →
(seqω((𝑘
∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣) ∈ On) |
66 | 65 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺)) → (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣) ∈ On) |
67 | | ovres 7379 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ dom 𝐺 ∧ (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣) ∈ On) → (𝑣((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)) ↾ (dom 𝐺 × On))(seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣)) = (𝑣(𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))(seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣))) |
68 | 63, 66, 67 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺)) → (𝑣((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)) ↾ (dom 𝐺 × On))(seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣)) = (𝑣(𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))(seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣))) |
69 | 58, 68 | eqtr3id 2792 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺)) → (𝑣(𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))(seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣)) = (𝑣(𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))(seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣))) |
70 | 53, 69 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺)) → (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘suc 𝑣) = (𝑣(𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))(seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣))) |
71 | 51, 70 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺)) → ((𝐻‘suc 𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘suc 𝑣) ↔ (𝑣(𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))(𝐻‘𝑣)) = (𝑣(𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧))(seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣)))) |
72 | 49, 71 | syl5ibr 249 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑣 ∈ ω ∧ suc 𝑣 ⊆ dom 𝐺)) → ((𝐻‘𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣) → (𝐻‘suc 𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘suc 𝑣))) |
73 | 72 | expr 460 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → (suc 𝑣 ⊆ dom 𝐺 → ((𝐻‘𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣) → (𝐻‘suc 𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘suc 𝑣)))) |
74 | 73 | a2d 29 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((suc 𝑣 ⊆ dom 𝐺 → (𝐻‘𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣)) → (suc 𝑣 ⊆ dom 𝐺 → (𝐻‘suc 𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘suc 𝑣)))) |
75 | 48, 74 | syl5 34 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ ω) → ((𝑣 ⊆ dom 𝐺 → (𝐻‘𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣)) → (suc 𝑣 ⊆ dom 𝐺 → (𝐻‘suc 𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘suc 𝑣)))) |
76 | 75 | expcom 417 |
. . . . . 6
⊢ (𝑣 ∈ ω → (𝜑 → ((𝑣 ⊆ dom 𝐺 → (𝐻‘𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣)) → (suc 𝑣 ⊆ dom 𝐺 → (𝐻‘suc 𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘suc 𝑣))))) |
77 | 76 | a2d 29 |
. . . . 5
⊢ (𝑣 ∈ ω → ((𝜑 → (𝑣 ⊆ dom 𝐺 → (𝐻‘𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘𝑣))) → (𝜑 → (suc 𝑣 ⊆ dom 𝐺 → (𝐻‘suc 𝑣) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘suc 𝑣))))) |
78 | 24, 30, 36, 42, 44, 77 | finds 7681 |
. . . 4
⊢ (dom
𝐺 ∈ ω →
(𝜑 → (dom 𝐺 ⊆ dom 𝐺 → (𝐻‘dom 𝐺) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘dom 𝐺)))) |
79 | 10, 78 | mpcom 38 |
. . 3
⊢ (𝜑 → (dom 𝐺 ⊆ dom 𝐺 → (𝐻‘dom 𝐺) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘dom 𝐺))) |
80 | 8, 79 | mpi 20 |
. 2
⊢ (𝜑 → (𝐻‘dom 𝐺) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘dom 𝐺)) |
81 | 7, 80 | eqtrd 2777 |
1
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘𝐹) = (seqω((𝑘 ∈ dom 𝐺, 𝑧 ∈ On ↦ (((𝐴 ↑o (𝐺‘𝑘)) ·o (𝐹‘(𝐺‘𝑘))) +o 𝑧)), ∅)‘dom 𝐺)) |