cantnffval

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	cantnffval.s	$⊢ S = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
	cantnffval.a	$⊢ φ \to A \in On$
	cantnffval.b	$⊢ φ \to B \in On$
Assertion	cantnffval	$⊢ φ \to A CNF B = (f \in S ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h))$

Proof

Step	Hyp	Ref	Expression
1		cantnffval.s	$⊢ S = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
2		cantnffval.a	$⊢ φ \to A \in On$
3		cantnffval.b	$⊢ φ \to B \in On$
4		oveq12	$⊢ (x = A \land y = B) \to x^{y} = A^{B}$
5	4	rabeqdv	$⊢ (x = A \land y = B) \to \{g \in (x^{y}) \| {finSupp}_{\emptyset} (g)\} = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
6	5 1	eqtr4di	$⊢ (x = A \land y = B) \to \{g \in (x^{y}) \| {finSupp}_{\emptyset} (g)\} = S$
7		simp1l	$⊢ ((x = A \land y = B) \land k \in V \land z \in V) \to x = A$
8	7	oveq1d	$⊢ ((x = A \land y = B) \land k \in V \land z \in V) \to x ↑_{𝑜} h (k) = A ↑_{𝑜} h (k)$
9	8	oveq1d	$⊢ ((x = A \land y = B) \land k \in V \land z \in V) \to (x ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k)) = (A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))$
10	9	oveq1d	$⊢ ((x = A \land y = B) \land k \in V \land z \in V) \to ((x ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z = ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z$
11	10	mpoeq3dva	$⊢ (x = A \land y = B) \to (k \in V, z \in V ⟼ ((x ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z) = (k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z)$
12		eqid	$⊢ \emptyset = \emptyset$
13		seqomeq12	$⊢ ((k \in V, z \in V ⟼ ((x ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z) = (k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z) \land \emptyset = \emptyset) \to {seq}_{ω} ((k \in V, z \in V ⟼ ((x ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset)$
14	11 12 13	sylancl	$⊢ (x = A \land y = B) \to {seq}_{ω} ((k \in V, z \in V ⟼ ((x ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset)$
15	14	fveq1d	$⊢ (x = A \land y = B) \to {seq}_{ω} ((k \in V, z \in V ⟼ ((x ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h) = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h)$
16	15	csbeq2dv	$⊢ (x = A \land y = B) \to ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((x ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h) = ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h)$
17	6 16	mpteq12dv	$⊢ (x = A \land y = B) \to (f \in \{g \in (x^{y}) \| {finSupp}_{\emptyset} (g)\} ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((x ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h)) = (f \in S ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h))$
18		df-cnf	$⊢ CNF = (x \in On, y \in On ⟼ (f \in \{g \in (x^{y}) \| {finSupp}_{\emptyset} (g)\} ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((x ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h)))$
19		ovex	$⊢ A^{B} \in V$
20	1 19	rabex2	$⊢ S \in V$
21	20	mptex	$⊢ (f \in S ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h)) \in V$
22	17 18 21	ovmpoa	$⊢ (A \in On \land B \in On) \to A CNF B = (f \in S ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h))$
23	2 3 22	syl2anc	$⊢ φ \to A CNF B = (f \in S ⟼ ⦋ OrdIso (E, f supp \emptyset) / h ⦌ {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} h (k)) \cdot_{𝑜} f (h (k))) +_{𝑜} z), \emptyset) (dom h))$

Metamath Proof Explorer

Theorem cantnffval

Proof