Step | Hyp | Ref
| Expression |
1 | | cantnfrescl.d |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ∈ On) |
2 | | cantnfrescl.b |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ⊆ 𝐷) |
3 | | cantnfrescl.x |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (𝐷 ∖ 𝐵)) → 𝑋 = ∅) |
4 | 1, 2, 3 | extmptsuppeq 7319 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) = ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)) |
5 | | oieq2 8418 |
. . . . . . . . . . . 12
⊢ (((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) = ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅) → OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) = OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))) |
6 | 4, 5 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) = OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))) |
7 | 6 | fveq1d 6193 |
. . . . . . . . . 10
⊢ (𝜑 → (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘) = (OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) |
8 | 7 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘) = (OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) |
9 | 8 | oveq2d 6666 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → (𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) = (𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) |
10 | | suppssdm 7308 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) ⊆ dom (𝑛 ∈ 𝐵 ↦ 𝑋) |
11 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ 𝐵 ↦ 𝑋) = (𝑛 ∈ 𝐵 ↦ 𝑋) |
12 | 11 | dmmptss 5631 |
. . . . . . . . . . . . . 14
⊢ dom
(𝑛 ∈ 𝐵 ↦ 𝑋) ⊆ 𝐵 |
13 | 12 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom (𝑛 ∈ 𝐵 ↦ 𝑋) ⊆ 𝐵) |
14 | 10, 13 | syl5ss 3614 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) ⊆ 𝐵) |
15 | 14 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) ⊆ 𝐵) |
16 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ OrdIso( E
, ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) = OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) |
17 | 16 | oif 8435 |
. . . . . . . . . . . . 13
⊢ OrdIso( E
, ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)):dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))⟶((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) |
18 | 17 | ffvelrni 6358 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) → (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘) ∈ ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) |
19 | 18 | 3ad2ant2 1083 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘) ∈ ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) |
20 | 15, 19 | sseldd 3604 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘) ∈ 𝐵) |
21 | | fvres 6207 |
. . . . . . . . . 10
⊢ ((OrdIso(
E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘) ∈ 𝐵 → (((𝑛 ∈ 𝐷 ↦ 𝑋) ↾ 𝐵)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) = ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → (((𝑛 ∈ 𝐷 ↦ 𝑋) ↾ 𝐵)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) = ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) |
23 | 2 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → 𝐵 ⊆ 𝐷) |
24 | 23 | resmptd 5452 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → ((𝑛 ∈ 𝐷 ↦ 𝑋) ↾ 𝐵) = (𝑛 ∈ 𝐵 ↦ 𝑋)) |
25 | 24 | fveq1d 6193 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → (((𝑛 ∈ 𝐷 ↦ 𝑋) ↾ 𝐵)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) = ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) |
26 | 8 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) = ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) |
27 | 22, 25, 26 | 3eqtr3d 2664 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) = ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) |
28 | 9, 27 | oveq12d 6668 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → ((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) = ((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)))) |
29 | 28 | oveq1d 6665 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧) = (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)) |
30 | 29 | mpt2eq3dva 6719 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)) = (𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧))) |
31 | 6 | dmeqd 5326 |
. . . . . 6
⊢ (𝜑 → dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) = dom OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))) |
32 | | eqid 2622 |
. . . . . 6
⊢ On =
On |
33 | | mpt2eq12 6715 |
. . . . . 6
⊢ ((dom
OrdIso( E , ((𝑛 ∈
𝐵 ↦ 𝑋) supp ∅)) = dom OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)) ∧ On = On) →
(𝑘 ∈ dom OrdIso( E ,
((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)) = (𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧))) |
34 | 31, 32, 33 | sylancl 694 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)) = (𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧))) |
35 | 30, 34 | eqtrd 2656 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)) = (𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧))) |
36 | | eqid 2622 |
. . . 4
⊢ ∅ =
∅ |
37 | | seqomeq12 7549 |
. . . 4
⊢ (((𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)) = (𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)) ∧ ∅ = ∅) →
seq𝜔((𝑘
∈ dom OrdIso( E , ((𝑛
∈ 𝐵 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜
(OrdIso( E , ((𝑛 ∈
𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)), ∅)) |
38 | 35, 36, 37 | sylancl 694 |
. . 3
⊢ (𝜑 →
seq𝜔((𝑘
∈ dom OrdIso( E , ((𝑛
∈ 𝐵 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜
(OrdIso( E , ((𝑛 ∈
𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)), ∅)) |
39 | 38, 31 | fveq12d 6197 |
. 2
⊢ (𝜑 →
(seq𝜔((𝑘
∈ dom OrdIso( E , ((𝑛
∈ 𝐵 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜
(OrdIso( E , ((𝑛 ∈
𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))) =
(seq𝜔((𝑘
∈ dom OrdIso( E , ((𝑛
∈ 𝐷 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜
(OrdIso( E , ((𝑛 ∈
𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)))) |
40 | | cantnfs.s |
. . 3
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
41 | | cantnfs.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ On) |
42 | | cantnfs.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ On) |
43 | | cantnfres.m |
. . 3
⊢ (𝜑 → (𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆) |
44 | | eqid 2622 |
. . 3
⊢
seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) |
45 | 40, 41, 42, 16, 43, 44 | cantnfval2 8566 |
. 2
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑛 ∈ 𝐵 ↦ 𝑋)) = (seq𝜔((𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)))) |
46 | | cantnfrescl.t |
. . 3
⊢ 𝑇 = dom (𝐴 CNF 𝐷) |
47 | | eqid 2622 |
. . 3
⊢ OrdIso( E
, ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)) = OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)) |
48 | | cantnfrescl.a |
. . . . 5
⊢ (𝜑 → ∅ ∈ 𝐴) |
49 | 40, 41, 42, 1, 2, 3,
48, 46 | cantnfrescl 8573 |
. . . 4
⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆 ↔ (𝑛 ∈ 𝐷 ↦ 𝑋) ∈ 𝑇)) |
50 | 43, 49 | mpbid 222 |
. . 3
⊢ (𝜑 → (𝑛 ∈ 𝐷 ↦ 𝑋) ∈ 𝑇) |
51 | | eqid 2622 |
. . 3
⊢
seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) = seq𝜔((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)), ∅) |
52 | 46, 41, 1, 47, 50, 51 | cantnfval2 8566 |
. 2
⊢ (𝜑 → ((𝐴 CNF 𝐷)‘(𝑛 ∈ 𝐷 ↦ 𝑋)) = (seq𝜔((𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑𝑜 (OrdIso( E ,
((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·𝑜 ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +𝑜 𝑧)), ∅)‘dom OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)))) |
53 | 39, 45, 52 | 3eqtr4d 2666 |
1
⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑛 ∈ 𝐵 ↦ 𝑋)) = ((𝐴 CNF 𝐷)‘(𝑛 ∈ 𝐷 ↦ 𝑋))) |