cantnfval

Description: The value of the Cantor normal form function. (Contributed by Mario Carneiro, 25-May-2015) (Revised by AV, 28-Jun-2019)

	Ref	Expression
Hypotheses	cantnfs.s	$⊢ S = dom (A CNF B)$
	cantnfs.a	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
	cantnfcl.g	$⊢ G = OrdIso (E, F supp \emptyset)$
	cantnfcl.f	$⊢ φ \to F \in S$
	cantnfval.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset)$
Assertion	cantnfval	$⊢ φ \to (A CNF B) (F) = H (dom G)$

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		cantnfcl.g	$⊢ G = OrdIso (E, F supp \emptyset)$
5		cantnfcl.f	$⊢ φ \to F \in S$
6		cantnfval.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset)$
7		eqid	$⊢ \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
8	7 2 3	cantnffval	$⊢ φ \to A CNF B = (f \in \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h))$
9	8	fveq1d	$⊢ φ \to (A CNF B) (F) = (f \in \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h)) (F)$
10	7 2 3	cantnfdm	$⊢ φ \to dom (A CNF B) = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
11	1 10	eqtrid	$⊢ φ \to S = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
12	5 11	eleqtrd	$⊢ φ \to F \in \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
13		ovex	$⊢ f supp \emptyset \in V$
14		eqid	$⊢ OrdIso (E, f supp \emptyset) = OrdIso (E, f supp \emptyset)$
15	14	oiexg	$⊢ f supp \emptyset \in V \to OrdIso (E, f supp \emptyset) \in V$
16	13 15	mp1i	$⊢ f = F \to OrdIso (E, f supp \emptyset) \in V$
17		simpr	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to h = OrdIso (E, f supp \emptyset)$
18		oveq1	$⊢ f = F \to f supp \emptyset = F supp \emptyset$
19	18	adantr	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to f supp \emptyset = F supp \emptyset$
20		oieq2	$⊢ f supp \emptyset = F supp \emptyset \to OrdIso (E, f supp \emptyset) = OrdIso (E, F supp \emptyset)$
21	19 20	syl	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to OrdIso (E, f supp \emptyset) = OrdIso (E, F supp \emptyset)$
22	17 21	eqtrd	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to h = OrdIso (E, F supp \emptyset)$
23	22 4	eqtr4di	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to h = G$
24	23	fveq1d	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to h (k) = G (k)$
25	24	oveq2d	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to A ↑_{𝑜} h (k) = A ↑_{𝑜} G (k)$
26		simpl	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to f = F$
27	26 24	fveq12d	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to f (h (k)) = F (G (k))$
28	25 27	oveq12d	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to (A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k)) = (A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))$
29	28	oveq1d	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z = ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z$
30	29	mpoeq3dv	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to (k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z) = (k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z)$
31		eqid	$⊢ \emptyset = \emptyset$
32		seqomeq12	$⊢ ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z) = (k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) \land \emptyset = \emptyset) \to {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset)$
33	30 31 32	sylancl	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset)$
34	33 6	eqtr4di	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) = H$
35	23	dmeqd	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to dom h = dom G$
36	34 35	fveq12d	$⊢ (f = F \land h = OrdIso (E, f supp \emptyset)) \to {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h) = H (dom G)$
37	16 36	csbied	$⊢ f = F \to ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h) = H (dom G)$
38		eqid	$⊢ (f \in \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h)) = (f \in \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h))$
39		fvex	$⊢ H (dom G) \in V$
40	37 38 39	fvmpt	$⊢ F \in \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} \to (f \in \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h)) (F) = H (dom G)$
41	12 40	syl	$⊢ φ \to (f \in \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h)) (F) = H (dom G)$
42	9 41	eqtrd	$⊢ φ \to (A CNF B) (F) = H (dom G)$

Metamath Proof Explorer

Theorem cantnfval

Proof