cantnfval2

Description: Alternate expression for 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	cantnfval2	$⊢ φ \to (A CNF B) (F) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (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	1 2 3 4 5 6	cantnfval	$⊢ φ \to (A CNF B) (F) = H (dom G)$
8		ssid	$⊢ dom G \subseteq dom G$
9	1 2 3 4 5	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (F) \land dom G \in ω)$
10	9	simprd	$⊢ φ \to dom G \in ω$
11		sseq1	$⊢ u = \emptyset \to (u \subseteq dom G \leftrightarrow \emptyset \subseteq dom G)$
12		fveq2	$⊢ u = \emptyset \to H (u) = H (\emptyset)$
13		0ex	$⊢ \emptyset \in V$
14	6	seqom0g	$⊢ \emptyset \in V \to H (\emptyset) = \emptyset$
15	13 14	ax-mp	$⊢ H (\emptyset) = \emptyset$
16	12 15	eqtrdi	$⊢ u = \emptyset \to H (u) = \emptyset$
17		fveq2	$⊢ u = \emptyset \to {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (\emptyset)$
18		eqid	$⊢ {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset)$
19	18	seqom0g	$⊢ \emptyset \in V \to {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (\emptyset) = \emptyset$
20	13 19	ax-mp	$⊢ {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (\emptyset) = \emptyset$
21	17 20	eqtrdi	$⊢ u = \emptyset \to {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u) = \emptyset$
22	16 21	eqeq12d	$⊢ u = \emptyset \to (H (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u) \leftrightarrow \emptyset = \emptyset)$
23	11 22	imbi12d	$⊢ u = \emptyset \to ((u \subseteq dom G \to H (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u)) \leftrightarrow (\emptyset \subseteq dom G \to \emptyset = \emptyset))$
24	23	imbi2d	$⊢ u = \emptyset \to ((φ \to (u \subseteq dom G \to H (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u))) \leftrightarrow (φ \to (\emptyset \subseteq dom G \to \emptyset = \emptyset)))$
25		sseq1	$⊢ u = v \to (u \subseteq dom G \leftrightarrow v \subseteq dom G)$
26		fveq2	$⊢ u = v \to H (u) = H (v)$
27		fveq2	$⊢ u = v \to {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v)$
28	26 27	eqeq12d	$⊢ u = v \to (H (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u) \leftrightarrow H (v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v))$
29	25 28	imbi12d	$⊢ u = v \to ((u \subseteq dom G \to H (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u)) \leftrightarrow (v \subseteq dom G \to H (v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v)))$
30	29	imbi2d	$⊢ u = v \to ((φ \to (u \subseteq dom G \to H (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u))) \leftrightarrow (φ \to (v \subseteq dom G \to H (v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v))))$
31		sseq1	$⊢ u = suc v \to (u \subseteq dom G \leftrightarrow suc v \subseteq dom G)$
32		fveq2	$⊢ u = suc v \to H (u) = H (suc v)$
33		fveq2	$⊢ u = suc v \to {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (suc v)$
34	32 33	eqeq12d	$⊢ u = suc v \to (H (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u) \leftrightarrow H (suc v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (suc v))$
35	31 34	imbi12d	$⊢ u = suc v \to ((u \subseteq dom G \to H (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u)) \leftrightarrow (suc v \subseteq dom G \to H (suc v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (suc v)))$
36	35	imbi2d	$⊢ u = suc v \to ((φ \to (u \subseteq dom G \to H (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u))) \leftrightarrow (φ \to (suc v \subseteq dom G \to H (suc v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (suc v))))$
37		sseq1	$⊢ u = dom G \to (u \subseteq dom G \leftrightarrow dom G \subseteq dom G)$
38		fveq2	$⊢ u = dom G \to H (u) = H (dom G)$
39		fveq2	$⊢ u = dom G \to {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (dom G)$
40	38 39	eqeq12d	$⊢ u = dom G \to (H (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u) \leftrightarrow H (dom G) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (dom G))$
41	37 40	imbi12d	$⊢ u = dom G \to ((u \subseteq dom G \to H (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u)) \leftrightarrow (dom G \subseteq dom G \to H (dom G) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (dom G)))$
42	41	imbi2d	$⊢ u = dom G \to ((φ \to (u \subseteq dom G \to H (u) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (u))) \leftrightarrow (φ \to (dom G \subseteq dom G \to H (dom G) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (dom G))))$
43		eqid	$⊢ \emptyset = \emptyset$
44	43	2a1i	$⊢ φ \to (\emptyset \subseteq dom G \to \emptyset = \emptyset)$
45		sssucid	$⊢ v \subseteq suc v$
46		sstr	$⊢ (v \subseteq suc v \land suc v \subseteq dom G) \to v \subseteq dom G$
47	45 46	mpan	$⊢ suc v \subseteq dom G \to v \subseteq dom G$
48	47	imim1i	$⊢ (v \subseteq dom G \to H (v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v)) \to (suc v \subseteq dom G \to H (v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v))$
49		oveq2	$⊢ H (v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v) \to v (k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) H (v) = v (k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v)$
50	6	seqomsuc	$⊢ v \in ω \to H (suc v) = v (k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) H (v)$
51	50	ad2antrl	$⊢ (φ \land (v \in ω \land suc v \subseteq dom G)) \to H (suc v) = v (k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) H (v)$
52	18	seqomsuc	$⊢ v \in ω \to {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (suc v) = v (k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v)$
53	52	ad2antrl	$⊢ (φ \land (v \in ω \land suc v \subseteq dom G)) \to {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (suc v) = v (k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v)$
54		ssv	$⊢ dom G \subseteq V$
55		ssv	$⊢ On \subseteq V$
56		resmpo	$⊢ (dom G \subseteq V \land On \subseteq V) \to {(k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) ↾}_{(dom G \times On)} = (k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z)$
57	54 55 56	mp2an	$⊢ {(k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) ↾}_{(dom G \times On)} = (k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z)$
58	57	oveqi	$⊢ v ({(k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) ↾}_{(dom G \times On)}) {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v) = v (k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v)$
59		simprr	$⊢ (φ \land (v \in ω \land suc v \subseteq dom G)) \to suc v \subseteq dom G$
60		vex	$⊢ v \in V$
61	60	sucid	$⊢ v \in suc v$
62	61	a1i	$⊢ (φ \land (v \in ω \land suc v \subseteq dom G)) \to v \in suc v$
63	59 62	sseldd	$⊢ (φ \land (v \in ω \land suc v \subseteq dom G)) \to v \in dom G$
64	18	cantnfvalf	$⊢ {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) : ω ⟶ On$
65	64	ffvelrni	$⊢ v \in ω \to {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v) \in On$
66	65	ad2antrl	$⊢ (φ \land (v \in ω \land suc v \subseteq dom G)) \to {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v) \in On$
67		ovres	$⊢ (v \in dom G \land {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v) \in On) \to v ({(k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) ↾}_{(dom G \times On)}) {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v) = v (k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v)$
68	63 66 67	syl2anc	$⊢ (φ \land (v \in ω \land suc v \subseteq dom G)) \to v ({(k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) ↾}_{(dom G \times On)}) {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v) = v (k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v)$
69	58 68	eqtr3id	$⊢ (φ \land (v \in ω \land suc v \subseteq dom G)) \to v (k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v) = v (k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v)$
70	53 69	eqtrd	$⊢ (φ \land (v \in ω \land suc v \subseteq dom G)) \to {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (suc v) = v (k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v)$
71	51 70	eqeq12d	$⊢ (φ \land (v \in ω \land suc v \subseteq dom G)) \to (H (suc v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (suc v) \leftrightarrow v (k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) H (v) = v (k \in V, z \in V ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v))$
72	49 71	syl5ibr	$⊢ (φ \land (v \in ω \land suc v \subseteq dom G)) \to (H (v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v) \to H (suc v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (suc v))$
73	72	expr	$⊢ (φ \land v \in ω) \to (suc v \subseteq dom G \to (H (v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v) \to H (suc v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (suc v)))$
74	73	a2d	$⊢ (φ \land v \in ω) \to ((suc v \subseteq dom G \to H (v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v)) \to (suc v \subseteq dom G \to H (suc v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (suc v)))$
75	48 74	syl5	$⊢ (φ \land v \in ω) \to ((v \subseteq dom G \to H (v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v)) \to (suc v \subseteq dom G \to H (suc v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (suc v)))$
76	75	expcom	$⊢ v \in ω \to (φ \to ((v \subseteq dom G \to H (v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v)) \to (suc v \subseteq dom G \to H (suc v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (suc v))))$
77	76	a2d	$⊢ v \in ω \to ((φ \to (v \subseteq dom G \to H (v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (v))) \to (φ \to (suc v \subseteq dom G \to H (suc v) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (suc v))))$
78	24 30 36 42 44 77	finds	$⊢ dom G \in ω \to (φ \to (dom G \subseteq dom G \to H (dom G) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (dom G)))$
79	10 78	mpcom	$⊢ φ \to (dom G \subseteq dom G \to H (dom G) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (dom G))$
80	8 79	mpi	$⊢ φ \to H (dom G) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (dom G)$
81	7 80	eqtrd	$⊢ φ \to (A CNF B) (F) = {seq}_{ω} ((k \in dom G, z \in On ⟼ ((A ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset) (dom G)$

Metamath Proof Explorer

Theorem cantnfval2

Proof