Metamath Proof Explorer

Theorem cantnfres

Description: The CNF function respects extensions of the domain to a larger ordinal. (Contributed by Mario Carneiro, 25-May-2015)

Ref Expression
Hypotheses cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
cantnfrescl.d ⊢ ( 𝜑 → 𝐷 ∈ On )
cantnfrescl.b ⊢ ( 𝜑 → 𝐵 ⊆ 𝐷 )
cantnfrescl.x ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐷 ∖ 𝐵 ) ) → 𝑋 = ∅ )
cantnfrescl.a ⊢ ( 𝜑 → ∅ ∈ 𝐴 )
cantnfrescl.t ⊢ 𝑇 = dom ( 𝐴 CNF 𝐷 )
cantnfres.m ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ 𝑆 )
Assertion cantnfres ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ) = ( ( 𝐴 CNF 𝐷 ) ‘ ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2 cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
3 cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
4 cantnfrescl.d ⊢ ( 𝜑 → 𝐷 ∈ On )
5 cantnfrescl.b ⊢ ( 𝜑 → 𝐵 ⊆ 𝐷 )
6 cantnfrescl.x ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝐷 ∖ 𝐵 ) ) → 𝑋 = ∅ )
7 cantnfrescl.a ⊢ ( 𝜑 → ∅ ∈ 𝐴 )
8 cantnfrescl.t ⊢ 𝑇 = dom ( 𝐴 CNF 𝐷 )
9 cantnfres.m ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ 𝑆 )
10 4 5 6 extmptsuppeq ⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) = ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) )
11 oieq2 ⊢ ( ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) = ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) → OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) = OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) )
12 10 11 syl ⊢ ( 𝜑 → OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) = OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) )
13 12 fveq1d ⊢ ( 𝜑 → ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) = ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) )
14 13 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ∧ 𝑧 ∈ On ) → ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) = ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) )
15 14 oveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ∧ 𝑧 ∈ On ) → ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) = ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) )
16 suppssdm ⊢ ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ⊆ dom ( 𝑛 ∈ 𝐵 ↦ 𝑋 )
17 eqid ⊢ ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) = ( 𝑛 ∈ 𝐵 ↦ 𝑋 )
18 17 dmmptss ⊢ dom ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ⊆ 𝐵
19 18 a1i ⊢ ( 𝜑 → dom ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ⊆ 𝐵 )
20 16 19 sstrid ⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ⊆ 𝐵 )
21 20 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ∧ 𝑧 ∈ On ) → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ⊆ 𝐵 )
22 eqid ⊢ OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) = OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) )
23 22 oif ⊢ OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) : dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ⟶ ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ )
24 23 ffvelrni ⊢ ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) → ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ∈ ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) )
25 24 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ∧ 𝑧 ∈ On ) → ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ∈ ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) )
26 21 25 sseldd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ∧ 𝑧 ∈ On ) → ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ∈ 𝐵 )
27 26 fvresd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ∧ 𝑧 ∈ On ) → ( ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ↾ 𝐵 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) = ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) )
28 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ∧ 𝑧 ∈ On ) → 𝐵 ⊆ 𝐷 )
29 28 resmptd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ∧ 𝑧 ∈ On ) → ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ↾ 𝐵 ) = ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) )
30 29 fveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ∧ 𝑧 ∈ On ) → ( ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ↾ 𝐵 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) = ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) )
31 14 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ∧ 𝑧 ∈ On ) → ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) = ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) )
32 27 30 31 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ∧ 𝑧 ∈ On ) → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) = ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) )
33 15 32 oveq12d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ∧ 𝑧 ∈ On ) → ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) = ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) )
34 33 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ∧ 𝑧 ∈ On ) → ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) = ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) )
35 34 mpoeq3dva ⊢ ( 𝜑 → ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) = ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) )
36 12 dmeqd ⊢ ( 𝜑 → dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) = dom OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) )
37 eqid ⊢ On = On
38 mpoeq12 ⊢ ( ( dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) = dom OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ∧ On = On ) → ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) = ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) )
39 36 37 38 sylancl ⊢ ( 𝜑 → ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) = ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) )
40 35 39 eqtrd ⊢ ( 𝜑 → ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) = ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) )
41 eqid ⊢ ∅ = ∅
42 seqomeq12 ⊢ ( ( ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) = ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) ∧ ∅ = ∅ ) → seqω ( ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) )
43 40 41 42 sylancl ⊢ ( 𝜑 → seqω ( ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) )
44 43 36 fveq12d ⊢ ( 𝜑 → ( seqω ( ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ) = ( seqω ( ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ) )
45 eqid ⊢ seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
46 1 2 3 22 9 45 cantnfval2 ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ) = ( seqω ( ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) supp ∅ ) ) ) )
47 eqid ⊢ OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) = OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) )
48 1 2 3 4 5 6 7 8 cantnfrescl ⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ∈ 𝑆 ↔ ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ∈ 𝑇 ) )
49 9 48 mpbid ⊢ ( 𝜑 → ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ∈ 𝑇 )
50 eqid ⊢ seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
51 8 2 4 47 49 50 cantnfval2 ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐷 ) ‘ ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ) = ( seqω ( ( 𝑘 ∈ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) , 𝑧 ∈ On ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ·o ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ‘ ( OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ( ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) supp ∅ ) ) ) )
52 44 46 51 3eqtr4d ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ ( 𝑛 ∈ 𝐵 ↦ 𝑋 ) ) = ( ( 𝐴 CNF 𝐷 ) ‘ ( 𝑛 ∈ 𝐷 ↦ 𝑋 ) ) )