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	$⊢ S = dom (A CNF B)$
	cantnfs.a	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
	cantnfrescl.d	$⊢ φ \to D \in On$
	cantnfrescl.b	$⊢ φ \to B \subseteq D$
	cantnfrescl.x	$⊢ (φ \land n \in (D ∖ B)) \to X = \emptyset$
	cantnfrescl.a	$⊢ φ \to \emptyset \in A$
	cantnfrescl.t	$⊢ T = dom (A CNF D)$
	cantnfres.m	$⊢ φ \to (n \in B ⟼ X) \in S$
Assertion	cantnfres	$⊢ φ \to (A CNF B) ((n \in B ⟼ X)) = (A CNF D) ((n \in D ⟼ X))$

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	$⊢ S = dom (A CNF B)$
2		cantnfs.a	$⊢ φ \to A \in On$
3		cantnfs.b	$⊢ φ \to B \in On$
4		cantnfrescl.d	$⊢ φ \to D \in On$
5		cantnfrescl.b	$⊢ φ \to B \subseteq D$
6		cantnfrescl.x	$⊢ (φ \land n \in (D ∖ B)) \to X = \emptyset$
7		cantnfrescl.a	$⊢ φ \to \emptyset \in A$
8		cantnfrescl.t	$⊢ T = dom (A CNF D)$
9		cantnfres.m	$⊢ φ \to (n \in B ⟼ X) \in S$
10	4 5 6	extmptsuppeq	$⊢ φ \to (n \in B ⟼ X) supp \emptyset = (n \in D ⟼ X) supp \emptyset$
11		oieq2	$⊢ (n \in B ⟼ X) supp \emptyset = (n \in D ⟼ X) supp \emptyset \to OrdIso (E, (n \in B ⟼ X) supp \emptyset) = OrdIso (E, (n \in D ⟼ X) supp \emptyset)$
12	10 11	syl	$⊢ φ \to OrdIso (E, (n \in B ⟼ X) supp \emptyset) = OrdIso (E, (n \in D ⟼ X) supp \emptyset)$
13	12	fveq1d	$⊢ φ \to OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k) = OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)$
14	13	3ad2ant1	$⊢ (φ \land k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) \land z \in On) \to OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k) = OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)$
15	14	oveq2d	$⊢ (φ \land k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) \land z \in On) \to A ↑_{𝑜} OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k) = A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)$
16		suppssdm	$⊢ (n \in B ⟼ X) supp \emptyset \subseteq dom (n \in B ⟼ X)$
17		eqid	$⊢ (n \in B ⟼ X) = (n \in B ⟼ X)$
18	17	dmmptss	$⊢ dom (n \in B ⟼ X) \subseteq B$
19	18	a1i	$⊢ φ \to dom (n \in B ⟼ X) \subseteq B$
20	16 19	sstrid	$⊢ φ \to (n \in B ⟼ X) supp \emptyset \subseteq B$
21	20	3ad2ant1	$⊢ (φ \land k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) \land z \in On) \to (n \in B ⟼ X) supp \emptyset \subseteq B$
22		eqid	$⊢ OrdIso (E, (n \in B ⟼ X) supp \emptyset) = OrdIso (E, (n \in B ⟼ X) supp \emptyset)$
23	22	oif	$⊢ OrdIso (E, (n \in B ⟼ X) supp \emptyset) : dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) ⟶ (n \in B ⟼ X) supp \emptyset$
24	23	ffvelcdmi	$⊢ k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) \to OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k) \in {supp}_{\emptyset} ((n \in B ⟼ X))$
25	24	3ad2ant2	$⊢ (φ \land k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) \land z \in On) \to OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k) \in {supp}_{\emptyset} ((n \in B ⟼ X))$
26	21 25	sseldd	$⊢ (φ \land k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) \land z \in On) \to OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k) \in B$
27	26	fvresd	$⊢ (φ \land k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) \land z \in On) \to ({(n \in D ⟼ X) ↾}_{B}) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) = (n \in D ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k))$
28	5	3ad2ant1	$⊢ (φ \land k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) \land z \in On) \to B \subseteq D$
29	28	resmptd	$⊢ (φ \land k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) \land z \in On) \to {(n \in D ⟼ X) ↾}_{B} = (n \in B ⟼ X)$
30	29	fveq1d	$⊢ (φ \land k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) \land z \in On) \to ({(n \in D ⟼ X) ↾}_{B}) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) = (n \in B ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k))$
31	14	fveq2d	$⊢ (φ \land k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) \land z \in On) \to (n \in D ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) = (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))$
32	27 30 31	3eqtr3d	$⊢ (φ \land k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) \land z \in On) \to (n \in B ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) = (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))$
33	15 32	oveq12d	$⊢ (φ \land k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) \land z \in On) \to (A ↑_{𝑜} OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in B ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) = (A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))$
34	33	oveq1d	$⊢ (φ \land k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) \land z \in On) \to ((A ↑_{𝑜} OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in B ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k))) +_{𝑜} z = ((A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))) +_{𝑜} z$
35	34	mpoeq3dva	$⊢ φ \to (k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in B ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k))) +_{𝑜} z) = (k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))) +_{𝑜} z)$
36	12	dmeqd	$⊢ φ \to dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) = dom OrdIso (E, (n \in D ⟼ X) supp \emptyset)$
37		eqid	$⊢ On = On$
38		mpoeq12	$⊢ (dom OrdIso (E, (n \in B ⟼ X) supp \emptyset) = dom OrdIso (E, (n \in D ⟼ X) supp \emptyset) \land On = On) \to (k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))) +_{𝑜} z) = (k \in dom OrdIso (E, (n \in D ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))) +_{𝑜} z)$
39	36 37 38	sylancl	$⊢ φ \to (k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))) +_{𝑜} z) = (k \in dom OrdIso (E, (n \in D ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))) +_{𝑜} z)$
40	35 39	eqtrd	$⊢ φ \to (k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in B ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k))) +_{𝑜} z) = (k \in dom OrdIso (E, (n \in D ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))) +_{𝑜} z)$
41		eqid	$⊢ \emptyset = \emptyset$
42		seqomeq12	$⊢ ((k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in B ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k))) +_{𝑜} z) = (k \in dom OrdIso (E, (n \in D ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))) +_{𝑜} z) \land \emptyset = \emptyset) \to {seq}_{ω} ((k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in B ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k))) +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in dom OrdIso (E, (n \in D ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))) +_{𝑜} z), \emptyset)$
43	40 41 42	sylancl	$⊢ φ \to {seq}_{ω} ((k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in B ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k))) +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in dom OrdIso (E, (n \in D ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))) +_{𝑜} z), \emptyset)$
44	43 36	fveq12d	$⊢ φ \to {seq}_{ω} ((k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in B ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k))) +_{𝑜} z), \emptyset) (dom OrdIso (E, (n \in B ⟼ X) supp \emptyset)) = {seq}_{ω} ((k \in dom OrdIso (E, (n \in D ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))) +_{𝑜} z), \emptyset) (dom OrdIso (E, (n \in D ⟼ X) supp \emptyset))$
45		eqid	$⊢ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in B ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k))) +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in B ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k))) +_{𝑜} z), \emptyset)$
46	1 2 3 22 9 45	cantnfval2	$⊢ φ \to (A CNF B) ((n \in B ⟼ X)) = {seq}_{ω} ((k \in dom OrdIso (E, (n \in B ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in B ⟼ X) (OrdIso (E, (n \in B ⟼ X) supp \emptyset) (k))) +_{𝑜} z), \emptyset) (dom OrdIso (E, (n \in B ⟼ X) supp \emptyset))$
47		eqid	$⊢ OrdIso (E, (n \in D ⟼ X) supp \emptyset) = OrdIso (E, (n \in D ⟼ X) supp \emptyset)$
48	1 2 3 4 5 6 7 8	cantnfrescl	$⊢ φ \to ((n \in B ⟼ X) \in S \leftrightarrow (n \in D ⟼ X) \in T)$
49	9 48	mpbid	$⊢ φ \to (n \in D ⟼ X) \in T$
50		eqid	$⊢ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))) +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))) +_{𝑜} z), \emptyset)$
51	8 2 4 47 49 50	cantnfval2	$⊢ φ \to (A CNF D) ((n \in D ⟼ X)) = {seq}_{ω} ((k \in dom OrdIso (E, (n \in D ⟼ X) supp \emptyset), z \in On ⟼ ((A ↑_{𝑜} OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k)) \cdot_{𝑜} (n \in D ⟼ X) (OrdIso (E, (n \in D ⟼ X) supp \emptyset) (k))) +_{𝑜} z), \emptyset) (dom OrdIso (E, (n \in D ⟼ X) supp \emptyset))$
52	44 46 51	3eqtr4d	$⊢ φ \to (A CNF B) ((n \in B ⟼ X)) = (A CNF D) ((n \in D ⟼ X))$

Metamath Proof Explorer

Theorem cantnfres

Proof