cantnfres - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cantnfres		Structured version Visualization version GIF version

Theorem cantnfres 9675

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

**Hypotheses**
Ref	Expression
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**
Ref	Expression
cantnfres	⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑛 ∈ 𝐵 ↦ 𝑋)) = ((𝐴 CNF 𝐷)‘(𝑛 ∈ 𝐷 ↦ 𝑋)))

Distinct variable groups: 𝐵,𝑛 𝐷,𝑛 𝐴,𝑛 𝜑,𝑛 Allowed substitution hints: 𝑆(𝑛) 𝑇(𝑛) 𝑋(𝑛)

Proof of Theorem cantnfres Dummy variables 𝑘 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cantnfrescl.d	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐷 ∈ On)
2		cantnfrescl.b	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐵 ⊆ 𝐷)
3		cantnfrescl.x	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑛 ∈ (𝐷 ∖ 𝐵)) → 𝑋 = ∅)
4	1, 2, 3	extmptsuppeq 8176	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) = ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))
5		oieq2 9511	. . . . . . . . . . . 12 ⊢ (((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) = ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅) → OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) = OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)))
6	4, 5	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) = OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)))
7	6	fveq1d 6894	. . . . . . . . . 10 ⊢ (𝜑 → (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘) = (OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))
8	7	3ad2ant1 1132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘) = (OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))
9	8	oveq2d 7428	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → (𝐴 ↑_o (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) = (𝐴 ↑_o (OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)))
10		suppssdm 8165	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) ⊆ dom (𝑛 ∈ 𝐵 ↦ 𝑋)
11		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ 𝐵 ↦ 𝑋) = (𝑛 ∈ 𝐵 ↦ 𝑋)
12	11	dmmptss 6241	. . . . . . . . . . . . . 14 ⊢ dom (𝑛 ∈ 𝐵 ↦ 𝑋) ⊆ 𝐵
13	12	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → dom (𝑛 ∈ 𝐵 ↦ 𝑋) ⊆ 𝐵)
14	10, 13	sstrid 3994	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) ⊆ 𝐵)
15	14	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅) ⊆ 𝐵)
16		eqid 2731	. . . . . . . . . . . . . 14 ⊢ OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) = OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))
17	16	oif 9528	. . . . . . . . . . . . 13 ⊢ OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)):dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))⟶((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)
18	17	ffvelcdmi 7086	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) → (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘) ∈ ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))
19	18	3ad2ant2 1133	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘) ∈ ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))
20	15, 19	sseldd 3984	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘) ∈ 𝐵)
21	20	fvresd 6912	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → (((𝑛 ∈ 𝐷 ↦ 𝑋) ↾ 𝐵)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) = ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)))
22	2	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → 𝐵 ⊆ 𝐷)
23	22	resmptd 6041	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → ((𝑛 ∈ 𝐷 ↦ 𝑋) ↾ 𝐵) = (𝑛 ∈ 𝐵 ↦ 𝑋))
24	23	fveq1d 6894	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → (((𝑛 ∈ 𝐷 ↦ 𝑋) ↾ 𝐵)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) = ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)))
25	8	fveq2d 6896	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) = ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)))
26	21, 24, 25	3eqtr3d 2779	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) = ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)))
27	9, 26	oveq12d 7430	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → ((𝐴 ↑_o (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·_o ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) = ((𝐴 ↑_o (OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·_o ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))))
28	27	oveq1d 7427	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) ∧ 𝑧 ∈ On) → (((𝐴 ↑_o (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·_o ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) +_o 𝑧) = (((𝐴 ↑_o (OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·_o ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +_o 𝑧))
29	28	mpoeq3dva 7489	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 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 𝑧)))
30	6	dmeqd 5906	. . . . . 6 ⊢ (𝜑 → dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)) = dom OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)))
31		eqid 2731	. . . . . 6 ⊢ On = On
32		mpoeq12 7485	. . . . . 6 ⊢ ((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 𝑧)))
33	30, 31, 32	sylancl 585	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ 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 𝑧)))
34	29, 33	eqtrd 2771	. . . 4 ⊢ (𝜑 → (𝑘 ∈ 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 𝑧)))
35		eqid 2731	. . . 4 ⊢ ∅ = ∅
36		seqomeq12 8457	. . . 4 ⊢ (((𝑘 ∈ 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 𝑧)), ∅))
37	34, 35, 36	sylancl 585	. . 3 ⊢ (𝜑 → 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 𝑧)), ∅))
38	37, 30	fveq12d 6899	. 2 ⊢ (𝜑 → (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 ∅))))
39		cantnfs.s	. . 3 ⊢ 𝑆 = dom (𝐴 CNF 𝐵)
40		cantnfs.a	. . 3 ⊢ (𝜑 → 𝐴 ∈ On)
41		cantnfs.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ On)
42		cantnfres.m	. . 3 ⊢ (𝜑 → (𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆)
43		eqid 2731	. . 3 ⊢ seq_ω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑_o (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·_o ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) +_o 𝑧)), ∅) = seq_ω((𝑘 ∈ V, 𝑧 ∈ V ↦ (((𝐴 ↑_o (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·_o ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) +_o 𝑧)), ∅)
44	39, 40, 41, 16, 42, 43	cantnfval2 9667	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑛 ∈ 𝐵 ↦ 𝑋)) = (seq_ω((𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑_o (OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘)) ·_o ((𝑛 ∈ 𝐵 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))‘𝑘))) +_o 𝑧)), ∅)‘dom OrdIso( E , ((𝑛 ∈ 𝐵 ↦ 𝑋) supp ∅))))
45		cantnfrescl.t	. . 3 ⊢ 𝑇 = dom (𝐴 CNF 𝐷)
46		eqid 2731	. . 3 ⊢ OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)) = OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))
47		cantnfrescl.a	. . . . 5 ⊢ (𝜑 → ∅ ∈ 𝐴)
48	39, 40, 41, 1, 2, 3, 47, 45	cantnfrescl 9674	. . . 4 ⊢ (𝜑 → ((𝑛 ∈ 𝐵 ↦ 𝑋) ∈ 𝑆 ↔ (𝑛 ∈ 𝐷 ↦ 𝑋) ∈ 𝑇))
49	42, 48	mpbid 231	. . 3 ⊢ (𝜑 → (𝑛 ∈ 𝐷 ↦ 𝑋) ∈ 𝑇)
50		eqid 2731	. . 3 ⊢ 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	45, 40, 1, 46, 49, 50	cantnfval2 9667	. 2 ⊢ (𝜑 → ((𝐴 CNF 𝐷)‘(𝑛 ∈ 𝐷 ↦ 𝑋)) = (seq_ω((𝑘 ∈ dom OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅)), 𝑧 ∈ On ↦ (((𝐴 ↑_o (OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘)) ·_o ((𝑛 ∈ 𝐷 ↦ 𝑋)‘(OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))‘𝑘))) +_o 𝑧)), ∅)‘dom OrdIso( E , ((𝑛 ∈ 𝐷 ↦ 𝑋) supp ∅))))
52	38, 44, 51	3eqtr4d 2781	1 ⊢ (𝜑 → ((𝐴 CNF 𝐵)‘(𝑛 ∈ 𝐵 ↦ 𝑋)) = ((𝐴 CNF 𝐷)‘(𝑛 ∈ 𝐷 ↦ 𝑋)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 Vcvv 3473 ∖ cdif 3946 ⊆ wss 3949 ∅c0 4323 ↦ cmpt 5232 E cep 5580 dom cdm 5677 ↾ cres 5679 Oncon0 6365 ‘cfv 6544 (class class class)co 7412 ∈ cmpo 7414 supp csupp 8149 seq_ωcseqom 8450 +_o coa 8466 ·_o comu 8467 ↑_o coe 8468 OrdIsocoi 9507 CNF ccnf 9659

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7728

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7859 df-1st 7978 df-2nd 7979 df-supp 8150 df-frecs 8269 df-wrecs 8300 df-recs 8374 df-rdg 8413 df-seqom 8451 df-1o 8469 df-oadd 8473 df-map 8825 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-fsupp 9365 df-oi 9508 df-cnf 9660

This theorem is referenced by: cantnf2 42378

W3C validator