cantnflem1

Description: Lemma for cantnf . This part of the proof is showing uniqueness of the Cantor normal form. We already know that the relation T is a strict order, but we haven't shown it is a well-order yet. But being a strict order is enough to show that two distinct F , G are T -related as F < G or G < F , and WLOG assuming that F < G , we show that CNF respects this order and maps these two to different ordinals. (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 2-Jul-2019)

	Ref	Expression
Hypotheses	cantnfs.s	$⊢ S = dom (A CNF B)$
	cantnfs.a	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
	oemapval.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\}$
	oemapval.f	$⊢ φ \to F \in S$
	oemapval.g	$⊢ φ \to G \in S$
	oemapvali.r	$⊢ φ \to F T G$
	oemapvali.x	$⊢ X = ⋃ \{c \in B \| F (c) \in G (c)\}$
	cantnflem1.o	$⊢ O = OrdIso (E, G supp \emptyset)$
	cantnflem1.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} O (k)) \cdot_{𝑜} G (O (k))) +_{𝑜} z), \emptyset)$
Assertion	cantnflem1	$⊢ φ \to (A CNF B) (F) \in (A CNF B) (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		oemapval.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\}$
5		oemapval.f	$⊢ φ \to F \in S$
6		oemapval.g	$⊢ φ \to G \in S$
7		oemapvali.r	$⊢ φ \to F T G$
8		oemapvali.x	$⊢ X = ⋃ \{c \in B \| F (c) \in G (c)\}$
9		cantnflem1.o	$⊢ O = OrdIso (E, G supp \emptyset)$
10		cantnflem1.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} O (k)) \cdot_{𝑜} G (O (k))) +_{𝑜} z), \emptyset)$
11		ovex	$⊢ G supp \emptyset \in V$
12	9	oion	$⊢ G supp \emptyset \in V \to dom O \in On$
13	11 12	mp1i	$⊢ φ \to dom O \in On$
14		uniexg	$⊢ dom O \in On \to ⋃ dom O \in V$
15		sucidg	$⊢ ⋃ dom O \in V \to ⋃ dom O \in suc ⋃ dom O$
16	13 14 15	3syl	$⊢ φ \to ⋃ dom O \in suc ⋃ dom O$
17	1 2 3 4 5 6 7 8	cantnflem1a	$⊢ φ \to X \in {supp}_{\emptyset} (G)$
18		n0i	$⊢ X \in {supp}_{\emptyset} (G) \to \neg G supp \emptyset = \emptyset$
19	17 18	syl	$⊢ φ \to \neg G supp \emptyset = \emptyset$
20		ovexd	$⊢ φ \to G supp \emptyset \in V$
21	1 2 3 9 6	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (G) \land dom O \in ω)$
22	21	simpld	$⊢ φ \to E We {supp}_{\emptyset} (G)$
23	9	oien	$⊢ (G supp \emptyset \in V \land E We {supp}_{\emptyset} (G)) \to dom O \approx {supp}_{\emptyset} (G)$
24	20 22 23	syl2anc	$⊢ φ \to dom O \approx {supp}_{\emptyset} (G)$
25		breq1	$⊢ dom O = \emptyset \to (dom O \approx {supp}_{\emptyset} (G) \leftrightarrow \emptyset \approx {supp}_{\emptyset} (G))$
26		ensymb	$⊢ \emptyset \approx {supp}_{\emptyset} (G) \leftrightarrow {supp}_{\emptyset} (G) \approx \emptyset$
27		en0	$⊢ {supp}_{\emptyset} (G) \approx \emptyset \leftrightarrow G supp \emptyset = \emptyset$
28	26 27	bitri	$⊢ \emptyset \approx {supp}_{\emptyset} (G) \leftrightarrow G supp \emptyset = \emptyset$
29	25 28	bitrdi	$⊢ dom O = \emptyset \to (dom O \approx {supp}_{\emptyset} (G) \leftrightarrow G supp \emptyset = \emptyset)$
30	24 29	syl5ibcom	$⊢ φ \to (dom O = \emptyset \to G supp \emptyset = \emptyset)$
31	19 30	mtod	$⊢ φ \to \neg dom O = \emptyset$
32	21	simprd	$⊢ φ \to dom O \in ω$
33		nnlim	$⊢ dom O \in ω \to \neg Lim dom O$
34	32 33	syl	$⊢ φ \to \neg Lim dom O$
35		ioran	$⊢ \neg (dom O = \emptyset \lor Lim dom O) \leftrightarrow (\neg dom O = \emptyset \land \neg Lim dom O)$
36	31 34 35	sylanbrc	$⊢ φ \to \neg (dom O = \emptyset \lor Lim dom O)$
37	9	oicl	$⊢ Ord dom O$
38		unizlim	$⊢ Ord dom O \to (dom O = ⋃ dom O \leftrightarrow (dom O = \emptyset \lor Lim dom O))$
39	37 38	mp1i	$⊢ φ \to (dom O = ⋃ dom O \leftrightarrow (dom O = \emptyset \lor Lim dom O))$
40	36 39	mtbird	$⊢ φ \to \neg dom O = ⋃ dom O$
41		orduniorsuc	$⊢ Ord dom O \to (dom O = ⋃ dom O \lor dom O = suc ⋃ dom O)$
42	37 41	mp1i	$⊢ φ \to (dom O = ⋃ dom O \lor dom O = suc ⋃ dom O)$
43	42	ord	$⊢ φ \to (\neg dom O = ⋃ dom O \to dom O = suc ⋃ dom O)$
44	40 43	mpd	$⊢ φ \to dom O = suc ⋃ dom O$
45	16 44	eleqtrrd	$⊢ φ \to ⋃ dom O \in dom O$
46	9	oiiso	$⊢ (G supp \emptyset \in V \land E We {supp}_{\emptyset} (G)) \to O {Isom}_{E, E} (dom O, G supp \emptyset)$
47	20 22 46	syl2anc	$⊢ φ \to O {Isom}_{E, E} (dom O, G supp \emptyset)$
48		isof1o	$⊢ O {Isom}_{E, E} (dom O, G supp \emptyset) \to O : dom O \underset{1-1 onto}{⟶} G supp \emptyset$
49	47 48	syl	$⊢ φ \to O : dom O \underset{1-1 onto}{⟶} G supp \emptyset$
50		f1ocnv	$⊢ O : dom O \underset{1-1 onto}{⟶} G supp \emptyset \to O^{-1} : G supp \emptyset \underset{1-1 onto}{⟶} dom O$
51		f1of	$⊢ O^{-1} : G supp \emptyset \underset{1-1 onto}{⟶} dom O \to O^{-1} : G supp \emptyset ⟶ dom O$
52	49 50 51	3syl	$⊢ φ \to O^{-1} : G supp \emptyset ⟶ dom O$
53	52 17	ffvelcdmd	$⊢ φ \to O^{-1} (X) \in dom O$
54		elssuni	$⊢ O^{-1} (X) \in dom O \to O^{-1} (X) \subseteq ⋃ dom O$
55	53 54	syl	$⊢ φ \to O^{-1} (X) \subseteq ⋃ dom O$
56	44 32	eqeltrrd	$⊢ φ \to suc ⋃ dom O \in ω$
57		peano2b	$⊢ ⋃ dom O \in ω \leftrightarrow suc ⋃ dom O \in ω$
58	56 57	sylibr	$⊢ φ \to ⋃ dom O \in ω$
59		eleq1	$⊢ y = ⋃ dom O \to (y \in dom O \leftrightarrow ⋃ dom O \in dom O)$
60		sseq2	$⊢ y = ⋃ dom O \to (O^{-1} (X) \subseteq y \leftrightarrow O^{-1} (X) \subseteq ⋃ dom O)$
61	59 60	anbi12d	$⊢ y = ⋃ dom O \to ((y \in dom O \land O^{-1} (X) \subseteq y) \leftrightarrow (⋃ dom O \in dom O \land O^{-1} (X) \subseteq ⋃ dom O))$
62		fveq2	$⊢ y = ⋃ dom O \to O (y) = O (⋃ dom O)$
63	62	sseq2d	$⊢ y = ⋃ dom O \to (x \subseteq O (y) \leftrightarrow x \subseteq O (⋃ dom O))$
64	63	ifbid	$⊢ y = ⋃ dom O \to if (x \subseteq O (y), F (x), \emptyset) = if (x \subseteq O (⋃ dom O), F (x), \emptyset)$
65	64	mpteq2dv	$⊢ y = ⋃ dom O \to (x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset)) = (x \in B ⟼ if (x \subseteq O (⋃ dom O), F (x), \emptyset))$
66	65	fveq2d	$⊢ y = ⋃ dom O \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset))) = (A CNF B) ((x \in B ⟼ if (x \subseteq O (⋃ dom O), F (x), \emptyset)))$
67		suceq	$⊢ y = ⋃ dom O \to suc y = suc ⋃ dom O$
68	67	fveq2d	$⊢ y = ⋃ dom O \to H (suc y) = H (suc ⋃ dom O)$
69	66 68	eleq12d	$⊢ y = ⋃ dom O \to ((A CNF B) ((x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset))) \in H (suc y) \leftrightarrow (A CNF B) ((x \in B ⟼ if (x \subseteq O (⋃ dom O), F (x), \emptyset))) \in H (suc ⋃ dom O))$
70	61 69	imbi12d	$⊢ y = ⋃ dom O \to (((y \in dom O \land O^{-1} (X) \subseteq y) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset))) \in H (suc y)) \leftrightarrow ((⋃ dom O \in dom O \land O^{-1} (X) \subseteq ⋃ dom O) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (⋃ dom O), F (x), \emptyset))) \in H (suc ⋃ dom O)))$
71	70	imbi2d	$⊢ y = ⋃ dom O \to ((φ \to ((y \in dom O \land O^{-1} (X) \subseteq y) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset))) \in H (suc y))) \leftrightarrow (φ \to ((⋃ dom O \in dom O \land O^{-1} (X) \subseteq ⋃ dom O) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (⋃ dom O), F (x), \emptyset))) \in H (suc ⋃ dom O))))$
72		eleq1	$⊢ y = \emptyset \to (y \in dom O \leftrightarrow \emptyset \in dom O)$
73		sseq2	$⊢ y = \emptyset \to (O^{-1} (X) \subseteq y \leftrightarrow O^{-1} (X) \subseteq \emptyset)$
74	72 73	anbi12d	$⊢ y = \emptyset \to ((y \in dom O \land O^{-1} (X) \subseteq y) \leftrightarrow (\emptyset \in dom O \land O^{-1} (X) \subseteq \emptyset))$
75		fveq2	$⊢ y = \emptyset \to O (y) = O (\emptyset)$
76	75	sseq2d	$⊢ y = \emptyset \to (x \subseteq O (y) \leftrightarrow x \subseteq O (\emptyset))$
77	76	ifbid	$⊢ y = \emptyset \to if (x \subseteq O (y), F (x), \emptyset) = if (x \subseteq O (\emptyset), F (x), \emptyset)$
78	77	mpteq2dv	$⊢ y = \emptyset \to (x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset)) = (x \in B ⟼ if (x \subseteq O (\emptyset), F (x), \emptyset))$
79	78	fveq2d	$⊢ y = \emptyset \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset))) = (A CNF B) ((x \in B ⟼ if (x \subseteq O (\emptyset), F (x), \emptyset)))$
80		suceq	$⊢ y = \emptyset \to suc y = suc \emptyset$
81	80	fveq2d	$⊢ y = \emptyset \to H (suc y) = H (suc \emptyset)$
82	79 81	eleq12d	$⊢ y = \emptyset \to ((A CNF B) ((x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset))) \in H (suc y) \leftrightarrow (A CNF B) ((x \in B ⟼ if (x \subseteq O (\emptyset), F (x), \emptyset))) \in H (suc \emptyset))$
83	74 82	imbi12d	$⊢ y = \emptyset \to (((y \in dom O \land O^{-1} (X) \subseteq y) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset))) \in H (suc y)) \leftrightarrow ((\emptyset \in dom O \land O^{-1} (X) \subseteq \emptyset) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (\emptyset), F (x), \emptyset))) \in H (suc \emptyset)))$
84		eleq1	$⊢ y = u \to (y \in dom O \leftrightarrow u \in dom O)$
85		sseq2	$⊢ y = u \to (O^{-1} (X) \subseteq y \leftrightarrow O^{-1} (X) \subseteq u)$
86	84 85	anbi12d	$⊢ y = u \to ((y \in dom O \land O^{-1} (X) \subseteq y) \leftrightarrow (u \in dom O \land O^{-1} (X) \subseteq u))$
87		fveq2	$⊢ y = u \to O (y) = O (u)$
88	87	sseq2d	$⊢ y = u \to (x \subseteq O (y) \leftrightarrow x \subseteq O (u))$
89	88	ifbid	$⊢ y = u \to if (x \subseteq O (y), F (x), \emptyset) = if (x \subseteq O (u), F (x), \emptyset)$
90	89	mpteq2dv	$⊢ y = u \to (x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset)) = (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))$
91	90	fveq2d	$⊢ y = u \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset))) = (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)))$
92		suceq	$⊢ y = u \to suc y = suc u$
93	92	fveq2d	$⊢ y = u \to H (suc y) = H (suc u)$
94	91 93	eleq12d	$⊢ y = u \to ((A CNF B) ((x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset))) \in H (suc y) \leftrightarrow (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u))$
95	86 94	imbi12d	$⊢ y = u \to (((y \in dom O \land O^{-1} (X) \subseteq y) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset))) \in H (suc y)) \leftrightarrow ((u \in dom O \land O^{-1} (X) \subseteq u) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u)))$
96		eleq1	$⊢ y = suc u \to (y \in dom O \leftrightarrow suc u \in dom O)$
97		sseq2	$⊢ y = suc u \to (O^{-1} (X) \subseteq y \leftrightarrow O^{-1} (X) \subseteq suc u)$
98	96 97	anbi12d	$⊢ y = suc u \to ((y \in dom O \land O^{-1} (X) \subseteq y) \leftrightarrow (suc u \in dom O \land O^{-1} (X) \subseteq suc u))$
99		fveq2	$⊢ y = suc u \to O (y) = O (suc u)$
100	99	sseq2d	$⊢ y = suc u \to (x \subseteq O (y) \leftrightarrow x \subseteq O (suc u))$
101	100	ifbid	$⊢ y = suc u \to if (x \subseteq O (y), F (x), \emptyset) = if (x \subseteq O (suc u), F (x), \emptyset)$
102	101	mpteq2dv	$⊢ y = suc u \to (x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset)) = (x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))$
103	102	fveq2d	$⊢ y = suc u \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset))) = (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset)))$
104		suceq	$⊢ y = suc u \to suc y = suc suc u$
105	104	fveq2d	$⊢ y = suc u \to H (suc y) = H (suc suc u)$
106	103 105	eleq12d	$⊢ y = suc u \to ((A CNF B) ((x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset))) \in H (suc y) \leftrightarrow (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u))$
107	98 106	imbi12d	$⊢ y = suc u \to (((y \in dom O \land O^{-1} (X) \subseteq y) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset))) \in H (suc y)) \leftrightarrow ((suc u \in dom O \land O^{-1} (X) \subseteq suc u) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u)))$
108		f1ocnvfv2	$⊢ (O : dom O \underset{1-1 onto}{⟶} G supp \emptyset \land X \in {supp}_{\emptyset} (G)) \to O (O^{-1} (X)) = X$
109	49 17 108	syl2anc	$⊢ φ \to O (O^{-1} (X)) = X$
110	109	sseq2d	$⊢ φ \to (x \subseteq O (O^{-1} (X)) \leftrightarrow x \subseteq X)$
111	110	ifbid	$⊢ φ \to if (x \subseteq O (O^{-1} (X)), F (x), \emptyset) = if (x \subseteq X, F (x), \emptyset)$
112	111	mpteq2dv	$⊢ φ \to (x \in B ⟼ if (x \subseteq O (O^{-1} (X)), F (x), \emptyset)) = (x \in B ⟼ if (x \subseteq X, F (x), \emptyset))$
113	112	fveq2d	$⊢ φ \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (O^{-1} (X)), F (x), \emptyset))) = (A CNF B) ((x \in B ⟼ if (x \subseteq X, F (x), \emptyset)))$
114	1 2 3 4 5 6 7 8 9 10	cantnflem1d	$⊢ φ \to (A CNF B) ((x \in B ⟼ if (x \subseteq X, F (x), \emptyset))) \in H (suc O^{-1} (X))$
115	113 114	eqeltrd	$⊢ φ \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (O^{-1} (X)), F (x), \emptyset))) \in H (suc O^{-1} (X))$
116		ss0	$⊢ O^{-1} (X) \subseteq \emptyset \to O^{-1} (X) = \emptyset$
117	116	fveq2d	$⊢ O^{-1} (X) \subseteq \emptyset \to O (O^{-1} (X)) = O (\emptyset)$
118	117	sseq2d	$⊢ O^{-1} (X) \subseteq \emptyset \to (x \subseteq O (O^{-1} (X)) \leftrightarrow x \subseteq O (\emptyset))$
119	118	ifbid	$⊢ O^{-1} (X) \subseteq \emptyset \to if (x \subseteq O (O^{-1} (X)), F (x), \emptyset) = if (x \subseteq O (\emptyset), F (x), \emptyset)$
120	119	mpteq2dv	$⊢ O^{-1} (X) \subseteq \emptyset \to (x \in B ⟼ if (x \subseteq O (O^{-1} (X)), F (x), \emptyset)) = (x \in B ⟼ if (x \subseteq O (\emptyset), F (x), \emptyset))$
121	120	fveq2d	$⊢ O^{-1} (X) \subseteq \emptyset \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (O^{-1} (X)), F (x), \emptyset))) = (A CNF B) ((x \in B ⟼ if (x \subseteq O (\emptyset), F (x), \emptyset)))$
122		suceq	$⊢ O^{-1} (X) = \emptyset \to suc O^{-1} (X) = suc \emptyset$
123	116 122	syl	$⊢ O^{-1} (X) \subseteq \emptyset \to suc O^{-1} (X) = suc \emptyset$
124	123	fveq2d	$⊢ O^{-1} (X) \subseteq \emptyset \to H (suc O^{-1} (X)) = H (suc \emptyset)$
125	121 124	eleq12d	$⊢ O^{-1} (X) \subseteq \emptyset \to ((A CNF B) ((x \in B ⟼ if (x \subseteq O (O^{-1} (X)), F (x), \emptyset))) \in H (suc O^{-1} (X)) \leftrightarrow (A CNF B) ((x \in B ⟼ if (x \subseteq O (\emptyset), F (x), \emptyset))) \in H (suc \emptyset))$
126	125	adantl	$⊢ (\emptyset \in dom O \land O^{-1} (X) \subseteq \emptyset) \to ((A CNF B) ((x \in B ⟼ if (x \subseteq O (O^{-1} (X)), F (x), \emptyset))) \in H (suc O^{-1} (X)) \leftrightarrow (A CNF B) ((x \in B ⟼ if (x \subseteq O (\emptyset), F (x), \emptyset))) \in H (suc \emptyset))$
127	115 126	syl5ibcom	$⊢ φ \to ((\emptyset \in dom O \land O^{-1} (X) \subseteq \emptyset) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (\emptyset), F (x), \emptyset))) \in H (suc \emptyset))$
128		ordelon	$⊢ (Ord dom O \land O^{-1} (X) \in dom O) \to O^{-1} (X) \in On$
129	37 53 128	sylancr	$⊢ φ \to O^{-1} (X) \in On$
130	37	a1i	$⊢ φ \to Ord dom O$
131		ordelon	$⊢ (Ord dom O \land suc u \in dom O) \to suc u \in On$
132	130 131	sylan	$⊢ (φ \land suc u \in dom O) \to suc u \in On$
133		onsseleq	$⊢ (O^{-1} (X) \in On \land suc u \in On) \to (O^{-1} (X) \subseteq suc u \leftrightarrow (O^{-1} (X) \in suc u \lor O^{-1} (X) = suc u))$
134	129 132 133	syl2an2r	$⊢ (φ \land suc u \in dom O) \to (O^{-1} (X) \subseteq suc u \leftrightarrow (O^{-1} (X) \in suc u \lor O^{-1} (X) = suc u))$
135		onsucb	$⊢ u \in On \leftrightarrow suc u \in On$
136	132 135	sylibr	$⊢ (φ \land suc u \in dom O) \to u \in On$
137		eloni	$⊢ u \in On \to Ord u$
138	136 137	syl	$⊢ (φ \land suc u \in dom O) \to Ord u$
139		ordsssuc	$⊢ (O^{-1} (X) \in On \land Ord u) \to (O^{-1} (X) \subseteq u \leftrightarrow O^{-1} (X) \in suc u)$
140	129 138 139	syl2an2r	$⊢ (φ \land suc u \in dom O) \to (O^{-1} (X) \subseteq u \leftrightarrow O^{-1} (X) \in suc u)$
141		ordtr	$⊢ Ord dom O \to Tr dom O$
142	37 141	mp1i	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to Tr dom O$
143		simprl	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to suc u \in dom O$
144		trsuc	$⊢ (Tr dom O \land suc u \in dom O) \to u \in dom O$
145	142 143 144	syl2anc	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to u \in dom O$
146		simprr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O^{-1} (X) \subseteq u$
147	145 146	jca	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (u \in dom O \land O^{-1} (X) \subseteq u)$
148	3	adantr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to B \in On$
149		oecl	$⊢ (A \in On \land B \in On) \to A ↑_{𝑜} B \in On$
150	2 148 149	syl2an2r	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to A ↑_{𝑜} B \in On$
151	2	adantr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to A \in On$
152	1 151 148	cantnff	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (A CNF B) : S ⟶ A ↑_{𝑜} B$
153	1 2 3	cantnfs	$⊢ φ \to (F \in S \leftrightarrow (F : B ⟶ A \land {finSupp}_{\emptyset} (F)))$
154	5 153	mpbid	$⊢ φ \to (F : B ⟶ A \land {finSupp}_{\emptyset} (F))$
155	154	simpld	$⊢ φ \to F : B ⟶ A$
156	155	ffvelcdmda	$⊢ (φ \land x \in B) \to F (x) \in A$
157	1 2 3	cantnfs	$⊢ φ \to (G \in S \leftrightarrow (G : B ⟶ A \land {finSupp}_{\emptyset} (G)))$
158	6 157	mpbid	$⊢ φ \to (G : B ⟶ A \land {finSupp}_{\emptyset} (G))$
159	158	simpld	$⊢ φ \to G : B ⟶ A$
160	1 2 3 4 5 6 7 8	oemapvali	$⊢ φ \to (X \in B \land F (X) \in G (X) \land \forall w \in B (X \in w \to F (w) = G (w)))$
161	160	simp1d	$⊢ φ \to X \in B$
162	159 161	ffvelcdmd	$⊢ φ \to G (X) \in A$
163	162	ne0d	$⊢ φ \to A \neq \emptyset$
164		on0eln0	$⊢ A \in On \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
165	2 164	syl	$⊢ φ \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
166	163 165	mpbird	$⊢ φ \to \emptyset \in A$
167	166	adantr	$⊢ (φ \land x \in B) \to \emptyset \in A$
168	156 167	ifcld	$⊢ (φ \land x \in B) \to if (x \subseteq O (u), F (x), \emptyset) \in A$
169	168	fmpttd	$⊢ φ \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) : B ⟶ A$
170	3	mptexd	$⊢ φ \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) \in V$
171		funmpt	$⊢ Fun (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))$
172	171	a1i	$⊢ φ \to Fun (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))$
173	154	simprd	$⊢ φ \to {finSupp}_{\emptyset} (F)$
174		ssidd	$⊢ φ \to F supp \emptyset \subseteq F supp \emptyset$
175		0ex	$⊢ \emptyset \in V$
176	175	a1i	$⊢ φ \to \emptyset \in V$
177	155 174 3 176	suppssr	$⊢ (φ \land x \in (B ∖ {supp}_{\emptyset} (F))) \to F (x) = \emptyset$
178	177	ifeq1d	$⊢ (φ \land x \in (B ∖ {supp}_{\emptyset} (F))) \to if (x \subseteq O (u), F (x), \emptyset) = if (x \subseteq O (u), \emptyset, \emptyset)$
179		ifid	$⊢ if (x \subseteq O (u), \emptyset, \emptyset) = \emptyset$
180	178 179	eqtrdi	$⊢ (φ \land x \in (B ∖ {supp}_{\emptyset} (F))) \to if (x \subseteq O (u), F (x), \emptyset) = \emptyset$
181	180 3	suppss2	$⊢ φ \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) supp \emptyset \subseteq F supp \emptyset$
182		fsuppsssupp	$⊢ (((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) \in V \land Fun (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \land ({finSupp}_{\emptyset} (F) \land (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) supp \emptyset \subseteq F supp \emptyset)) \to {finSupp}_{\emptyset} ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)))$
183	170 172 173 181 182	syl22anc	$⊢ φ \to {finSupp}_{\emptyset} ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)))$
184	1 2 3	cantnfs	$⊢ φ \to ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) \in S \leftrightarrow ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) : B ⟶ A \land {finSupp}_{\emptyset} ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)))))$
185	169 183 184	mpbir2and	$⊢ φ \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) \in S$
186	185	adantr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) \in S$
187	152 186	ffvelcdmd	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in (A ↑_{𝑜} B)$
188		onelon	$⊢ (A ↑_{𝑜} B \in On \land (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in (A ↑_{𝑜} B)) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in On$
189	150 187 188	syl2anc	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in On$
190	32	adantr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to dom O \in ω$
191		elnn	$⊢ (suc u \in dom O \land dom O \in ω) \to suc u \in ω$
192	143 190 191	syl2anc	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to suc u \in ω$
193	10	cantnfvalf	$⊢ H : ω ⟶ On$
194	193	ffvelcdmi	$⊢ suc u \in ω \to H (suc u) \in On$
195	192 194	syl	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to H (suc u) \in On$
196		suppssdm	$⊢ G supp \emptyset \subseteq dom G$
197	196 159	fssdm	$⊢ φ \to G supp \emptyset \subseteq B$
198	197	adantr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to G supp \emptyset \subseteq B$
199	9	oif	$⊢ O : dom O ⟶ G supp \emptyset$
200	199	ffvelcdmi	$⊢ suc u \in dom O \to O (suc u) \in {supp}_{\emptyset} (G)$
201	143 200	syl	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O (suc u) \in {supp}_{\emptyset} (G)$
202	198 201	sseldd	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O (suc u) \in B$
203		onelon	$⊢ (B \in On \land O (suc u) \in B) \to O (suc u) \in On$
204	3 202 203	syl2an2r	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O (suc u) \in On$
205		oecl	$⊢ (A \in On \land O (suc u) \in On) \to A ↑_{𝑜} O (suc u) \in On$
206	2 204 205	syl2an2r	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to A ↑_{𝑜} O (suc u) \in On$
207	155	adantr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to F : B ⟶ A$
208	207 202	ffvelcdmd	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to F (O (suc u)) \in A$
209		onelon	$⊢ (A \in On \land F (O (suc u)) \in A) \to F (O (suc u)) \in On$
210	2 208 209	syl2an2r	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to F (O (suc u)) \in On$
211		omcl	$⊢ (A ↑_{𝑜} O (suc u) \in On \land F (O (suc u)) \in On) \to (A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u)) \in On$
212	206 210 211	syl2anc	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u)) \in On$
213		oaord	$⊢ ((A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in On \land H (suc u) \in On \land (A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u)) \in On) \to ((A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u) \leftrightarrow ((A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u))) +_{𝑜} (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in (((A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u))) +_{𝑜} H (suc u)))$
214	189 195 212 213	syl3anc	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to ((A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u) \leftrightarrow ((A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u))) +_{𝑜} (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in (((A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u))) +_{𝑜} H (suc u)))$
215		ifeq1	$⊢ F (x) = \emptyset \to if (x \subseteq O (suc u), F (x), \emptyset) = if (x \subseteq O (suc u), \emptyset, \emptyset)$
216		ifid	$⊢ if (x \subseteq O (suc u), \emptyset, \emptyset) = \emptyset$
217	215 216	eqtrdi	$⊢ F (x) = \emptyset \to if (x \subseteq O (suc u), F (x), \emptyset) = \emptyset$
218		ifeq1	$⊢ F (x) = \emptyset \to if ((x = O (suc u) \lor x \subseteq O (u)), F (x), \emptyset) = if ((x = O (suc u) \lor x \subseteq O (u)), \emptyset, \emptyset)$
219		ifid	$⊢ if ((x = O (suc u) \lor x \subseteq O (u)), \emptyset, \emptyset) = \emptyset$
220	218 219	eqtrdi	$⊢ F (x) = \emptyset \to if ((x = O (suc u) \lor x \subseteq O (u)), F (x), \emptyset) = \emptyset$
221	217 220	eqeq12d	$⊢ F (x) = \emptyset \to (if (x \subseteq O (suc u), F (x), \emptyset) = if ((x = O (suc u) \lor x \subseteq O (u)), F (x), \emptyset) \leftrightarrow \emptyset = \emptyset)$
222		onss	$⊢ B \in On \to B \subseteq On$
223	3 222	syl	$⊢ φ \to B \subseteq On$
224	223	sselda	$⊢ (φ \land x \in B) \to x \in On$
225	224	adantlr	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \to x \in On$
226	204	adantr	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \to O (suc u) \in On$
227		onsseleq	$⊢ (x \in On \land O (suc u) \in On) \to (x \subseteq O (suc u) \leftrightarrow (x \in O (suc u) \lor x = O (suc u)))$
228	225 226 227	syl2anc	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \to (x \subseteq O (suc u) \leftrightarrow (x \in O (suc u) \lor x = O (suc u)))$
229	228	adantr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to (x \subseteq O (suc u) \leftrightarrow (x \in O (suc u) \lor x = O (suc u)))$
230	199	ffvelcdmi	$⊢ u \in dom O \to O (u) \in {supp}_{\emptyset} (G)$
231	145 230	syl	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O (u) \in {supp}_{\emptyset} (G)$
232	198 231	sseldd	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O (u) \in B$
233		onelon	$⊢ (B \in On \land O (u) \in B) \to O (u) \in On$
234	3 232 233	syl2an2r	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O (u) \in On$
235	234	ad2antrr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to O (u) \in On$
236		onsssuc	$⊢ (x \in On \land O (u) \in On) \to (x \subseteq O (u) \leftrightarrow x \in suc O (u))$
237	225 235 236	syl2an2r	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to (x \subseteq O (u) \leftrightarrow x \in suc O (u))$
238		vex	$⊢ u \in V$
239	238	sucid	$⊢ u \in suc u$
240	47	adantr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O {Isom}_{E, E} (dom O, G supp \emptyset)$
241		isorel	$⊢ (O {Isom}_{E, E} (dom O, G supp \emptyset) \land (u \in dom O \land suc u \in dom O)) \to (u E suc u \leftrightarrow O (u) E O (suc u))$
242	240 145 143 241	syl12anc	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (u E suc u \leftrightarrow O (u) E O (suc u))$
243	238	sucex	$⊢ suc u \in V$
244	243	epeli	$⊢ u E suc u \leftrightarrow u \in suc u$
245		fvex	$⊢ O (suc u) \in V$
246	245	epeli	$⊢ O (u) E O (suc u) \leftrightarrow O (u) \in O (suc u)$
247	242 244 246	3bitr3g	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (u \in suc u \leftrightarrow O (u) \in O (suc u))$
248	239 247	mpbii	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O (u) \in O (suc u)$
249		eloni	$⊢ O (suc u) \in On \to Ord O (suc u)$
250	204 249	syl	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to Ord O (suc u)$
251		ordelsuc	$⊢ (O (u) \in On \land Ord O (suc u)) \to (O (u) \in O (suc u) \leftrightarrow suc O (u) \subseteq O (suc u))$
252	234 250 251	syl2anc	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (O (u) \in O (suc u) \leftrightarrow suc O (u) \subseteq O (suc u))$
253	248 252	mpbid	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to suc O (u) \subseteq O (suc u)$
254	253	ad2antrr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to suc O (u) \subseteq O (suc u)$
255	254	sseld	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to (x \in suc O (u) \to x \in O (suc u))$
256	237 255	sylbid	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to (x \subseteq O (u) \to x \in O (suc u))$
257		simprr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to O (u) \in x$
258	240	ad2antrr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to O {Isom}_{E, E} (dom O, G supp \emptyset)$
259	258 48	syl	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to O : dom O \underset{1-1 onto}{⟶} G supp \emptyset$
260	1 2 3 4 5 6 7 8 9	cantnflem1c	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to x \in {supp}_{\emptyset} (G)$
261		f1ocnvfv2	$⊢ (O : dom O \underset{1-1 onto}{⟶} G supp \emptyset \land x \in {supp}_{\emptyset} (G)) \to O (O^{-1} (x)) = x$
262	259 260 261	syl2anc	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to O (O^{-1} (x)) = x$
263	257 262	eleqtrrd	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to O (u) \in O (O^{-1} (x))$
264	145	ad2antrr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to u \in dom O$
265	259 50 51	3syl	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to O^{-1} : G supp \emptyset ⟶ dom O$
266	265 260	ffvelcdmd	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to O^{-1} (x) \in dom O$
267		isorel	$⊢ (O {Isom}_{E, E} (dom O, G supp \emptyset) \land (u \in dom O \land O^{-1} (x) \in dom O)) \to (u E O^{-1} (x) \leftrightarrow O (u) E O (O^{-1} (x)))$
268	258 264 266 267	syl12anc	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to (u E O^{-1} (x) \leftrightarrow O (u) E O (O^{-1} (x)))$
269		fvex	$⊢ O^{-1} (x) \in V$
270	269	epeli	$⊢ u E O^{-1} (x) \leftrightarrow u \in O^{-1} (x)$
271		fvex	$⊢ O (O^{-1} (x)) \in V$
272	271	epeli	$⊢ O (u) E O (O^{-1} (x)) \leftrightarrow O (u) \in O (O^{-1} (x))$
273	268 270 272	3bitr3g	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to (u \in O^{-1} (x) \leftrightarrow O (u) \in O (O^{-1} (x)))$
274	263 273	mpbird	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to u \in O^{-1} (x)$
275		ordelon	$⊢ (Ord dom O \land O^{-1} (x) \in dom O) \to O^{-1} (x) \in On$
276	37 266 275	sylancr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to O^{-1} (x) \in On$
277		eloni	$⊢ O^{-1} (x) \in On \to Ord O^{-1} (x)$
278	276 277	syl	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to Ord O^{-1} (x)$
279		ordelsuc	$⊢ (u \in O^{-1} (x) \land Ord O^{-1} (x)) \to (u \in O^{-1} (x) \leftrightarrow suc u \subseteq O^{-1} (x))$
280	274 278 279	syl2anc	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to (u \in O^{-1} (x) \leftrightarrow suc u \subseteq O^{-1} (x))$
281	274 280	mpbid	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to suc u \subseteq O^{-1} (x)$
282	143	ad2antrr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to suc u \in dom O$
283	37 282 131	sylancr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to suc u \in On$
284		ontri1	$⊢ (suc u \in On \land O^{-1} (x) \in On) \to (suc u \subseteq O^{-1} (x) \leftrightarrow \neg O^{-1} (x) \in suc u)$
285	283 276 284	syl2anc	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to (suc u \subseteq O^{-1} (x) \leftrightarrow \neg O^{-1} (x) \in suc u)$
286	281 285	mpbid	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to \neg O^{-1} (x) \in suc u$
287		isorel	$⊢ (O {Isom}_{E, E} (dom O, G supp \emptyset) \land (O^{-1} (x) \in dom O \land suc u \in dom O)) \to (O^{-1} (x) E suc u \leftrightarrow O (O^{-1} (x)) E O (suc u))$
288	258 266 282 287	syl12anc	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to (O^{-1} (x) E suc u \leftrightarrow O (O^{-1} (x)) E O (suc u))$
289	243	epeli	$⊢ O^{-1} (x) E suc u \leftrightarrow O^{-1} (x) \in suc u$
290	245	epeli	$⊢ O (O^{-1} (x)) E O (suc u) \leftrightarrow O (O^{-1} (x)) \in O (suc u)$
291	288 289 290	3bitr3g	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to (O^{-1} (x) \in suc u \leftrightarrow O (O^{-1} (x)) \in O (suc u))$
292	262	eleq1d	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to (O (O^{-1} (x)) \in O (suc u) \leftrightarrow x \in O (suc u))$
293	291 292	bitrd	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to (O^{-1} (x) \in suc u \leftrightarrow x \in O (suc u))$
294	286 293	mtbid	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land (F (x) \neq \emptyset \land O (u) \in x)) \to \neg x \in O (suc u)$
295	294	expr	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to (O (u) \in x \to \neg x \in O (suc u))$
296	295	con2d	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to (x \in O (suc u) \to \neg O (u) \in x)$
297		ontri1	$⊢ (x \in On \land O (u) \in On) \to (x \subseteq O (u) \leftrightarrow \neg O (u) \in x)$
298	225 235 297	syl2an2r	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to (x \subseteq O (u) \leftrightarrow \neg O (u) \in x)$
299	296 298	sylibrd	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to (x \in O (suc u) \to x \subseteq O (u))$
300	256 299	impbid	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to (x \subseteq O (u) \leftrightarrow x \in O (suc u))$
301	300	orbi1d	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to ((x \subseteq O (u) \lor x = O (suc u)) \leftrightarrow (x \in O (suc u) \lor x = O (suc u)))$
302	229 301	bitr4d	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to (x \subseteq O (suc u) \leftrightarrow (x \subseteq O (u) \lor x = O (suc u)))$
303		orcom	$⊢ (x \subseteq O (u) \lor x = O (suc u)) \leftrightarrow (x = O (suc u) \lor x \subseteq O (u))$
304	302 303	bitrdi	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to (x \subseteq O (suc u) \leftrightarrow (x = O (suc u) \lor x \subseteq O (u)))$
305	304	ifbid	$⊢ (((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \land F (x) \neq \emptyset) \to if (x \subseteq O (suc u), F (x), \emptyset) = if ((x = O (suc u) \lor x \subseteq O (u)), F (x), \emptyset)$
306		eqidd	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \to \emptyset = \emptyset$
307	221 305 306	pm2.61ne	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \to if (x \subseteq O (suc u), F (x), \emptyset) = if ((x = O (suc u) \lor x \subseteq O (u)), F (x), \emptyset)$
308	307	mpteq2dva	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset)) = (x \in B ⟼ if ((x = O (suc u) \lor x \subseteq O (u)), F (x), \emptyset))$
309	308	fveq2d	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) = (A CNF B) ((x \in B ⟼ if ((x = O (suc u) \lor x \subseteq O (u)), F (x), \emptyset)))$
310		fvex	$⊢ F (x) \in V$
311	310 175	ifex	$⊢ if (x \subseteq O (u), F (x), \emptyset) \in V$
312	311	a1i	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to if (x \subseteq O (u), F (x), \emptyset) \in V$
313	312	ralrimivw	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to \forall x \in B if (x \subseteq O (u), F (x), \emptyset) \in V$
314		eqid	$⊢ (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) = (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))$
315	314	fnmpt	$⊢ \forall x \in B if (x \subseteq O (u), F (x), \emptyset) \in V \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) Fn B$
316	313 315	syl	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) Fn B$
317	175	a1i	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to \emptyset \in V$
318		suppvalfn	$⊢ ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) Fn B \land B \in On \land \emptyset \in V) \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) supp \emptyset = \{y \in B \| (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (y) \neq \emptyset\}$
319		nfcv	$⊢ \underline{Ⅎ} y B$
320		nfcv	$⊢ \underline{Ⅎ} x B$
321		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (y)$
322		nfcv	$⊢ \underline{Ⅎ} x \emptyset$
323	321 322	nfne	$⊢ Ⅎ x (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (y) \neq \emptyset$
324		nfv	$⊢ Ⅎ y (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (x) \neq \emptyset$
325		fveq2	$⊢ y = x \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (y) = (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (x)$
326	325	neeq1d	$⊢ y = x \to ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (y) \neq \emptyset \leftrightarrow (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (x) \neq \emptyset)$
327	319 320 323 324 326	cbvrabw	$⊢ \{y \in B \| (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (y) \neq \emptyset\} = \{x \in B \| (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (x) \neq \emptyset\}$
328	318 327	eqtrdi	$⊢ ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) Fn B \land B \in On \land \emptyset \in V) \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) supp \emptyset = \{x \in B \| (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (x) \neq \emptyset\}$
329	316 148 317 328	syl3anc	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) supp \emptyset = \{x \in B \| (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (x) \neq \emptyset\}$
330		eqidd	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) = (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))$
331	311	a1i	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \to if (x \subseteq O (u), F (x), \emptyset) \in V$
332	330 331	fvmpt2d	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (x) = if (x \subseteq O (u), F (x), \emptyset)$
333	332	neeq1d	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \to ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (x) \neq \emptyset \leftrightarrow if (x \subseteq O (u), F (x), \emptyset) \neq \emptyset)$
334	331	biantrurd	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \to (if (x \subseteq O (u), F (x), \emptyset) \neq \emptyset \leftrightarrow (if (x \subseteq O (u), F (x), \emptyset) \in V \land if (x \subseteq O (u), F (x), \emptyset) \neq \emptyset))$
335		dif1o	$⊢ if (x \subseteq O (u), F (x), \emptyset) \in (V ∖ 1_{𝑜}) \leftrightarrow (if (x \subseteq O (u), F (x), \emptyset) \in V \land if (x \subseteq O (u), F (x), \emptyset) \neq \emptyset)$
336	334 335	bitr4di	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \to (if (x \subseteq O (u), F (x), \emptyset) \neq \emptyset \leftrightarrow if (x \subseteq O (u), F (x), \emptyset) \in (V ∖ 1_{𝑜}))$
337	333 336	bitrd	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \to ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (x) \neq \emptyset \leftrightarrow if (x \subseteq O (u), F (x), \emptyset) \in (V ∖ 1_{𝑜}))$
338	337	rabbidva	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to \{x \in B \| (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (x) \neq \emptyset\} = \{x \in B \| if (x \subseteq O (u), F (x), \emptyset) \in (V ∖ 1_{𝑜})\}$
339	329 338	eqtrd	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) supp \emptyset = \{x \in B \| if (x \subseteq O (u), F (x), \emptyset) \in (V ∖ 1_{𝑜})\}$
340	311 335	mpbiran	$⊢ if (x \subseteq O (u), F (x), \emptyset) \in (V ∖ 1_{𝑜}) \leftrightarrow if (x \subseteq O (u), F (x), \emptyset) \neq \emptyset$
341		ifeq1	$⊢ F (x) = \emptyset \to if (x \subseteq O (u), F (x), \emptyset) = if (x \subseteq O (u), \emptyset, \emptyset)$
342	341 179	eqtrdi	$⊢ F (x) = \emptyset \to if (x \subseteq O (u), F (x), \emptyset) = \emptyset$
343	342	necon3i	$⊢ if (x \subseteq O (u), F (x), \emptyset) \neq \emptyset \to F (x) \neq \emptyset$
344		iffalse	$⊢ \neg x \subseteq O (u) \to if (x \subseteq O (u), F (x), \emptyset) = \emptyset$
345	344	necon1ai	$⊢ if (x \subseteq O (u), F (x), \emptyset) \neq \emptyset \to x \subseteq O (u)$
346	343 345	jca	$⊢ if (x \subseteq O (u), F (x), \emptyset) \neq \emptyset \to (F (x) \neq \emptyset \land x \subseteq O (u))$
347	256	expimpd	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \to ((F (x) \neq \emptyset \land x \subseteq O (u)) \to x \in O (suc u))$
348	346 347	syl5	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \to (if (x \subseteq O (u), F (x), \emptyset) \neq \emptyset \to x \in O (suc u))$
349	340 348	biimtrid	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B) \to (if (x \subseteq O (u), F (x), \emptyset) \in (V ∖ 1_{𝑜}) \to x \in O (suc u))$
350	349	3impia	$⊢ ((φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \land x \in B \land if (x \subseteq O (u), F (x), \emptyset) \in (V ∖ 1_{𝑜})) \to x \in O (suc u)$
351	350	rabssdv	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to \{x \in B \| if (x \subseteq O (u), F (x), \emptyset) \in (V ∖ 1_{𝑜})\} \subseteq O (suc u)$
352	339 351	eqsstrd	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) supp \emptyset \subseteq O (suc u)$
353		eqeq1	$⊢ x = y \to (x = O (suc u) \leftrightarrow y = O (suc u))$
354		sseq1	$⊢ x = y \to (x \subseteq O (u) \leftrightarrow y \subseteq O (u))$
355	353 354	orbi12d	$⊢ x = y \to ((x = O (suc u) \lor x \subseteq O (u)) \leftrightarrow (y = O (suc u) \lor y \subseteq O (u)))$
356		fveq2	$⊢ x = y \to F (x) = F (y)$
357	355 356	ifbieq1d	$⊢ x = y \to if ((x = O (suc u) \lor x \subseteq O (u)), F (x), \emptyset) = if ((y = O (suc u) \lor y \subseteq O (u)), F (y), \emptyset)$
358	357	cbvmptv	$⊢ (x \in B ⟼ if ((x = O (suc u) \lor x \subseteq O (u)), F (x), \emptyset)) = (y \in B ⟼ if ((y = O (suc u) \lor y \subseteq O (u)), F (y), \emptyset))$
359		fveq2	$⊢ y = O (suc u) \to F (y) = F (O (suc u))$
360	359	adantl	$⊢ (y \in B \land y = O (suc u)) \to F (y) = F (O (suc u))$
361	360	ifeq1da	$⊢ y \in B \to if (y = O (suc u), F (y), (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (y)) = if (y = O (suc u), F (O (suc u)), (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (y))$
362	354 356	ifbieq1d	$⊢ x = y \to if (x \subseteq O (u), F (x), \emptyset) = if (y \subseteq O (u), F (y), \emptyset)$
363		fvex	$⊢ F (y) \in V$
364	363 175	ifex	$⊢ if (y \subseteq O (u), F (y), \emptyset) \in V$
365	362 314 364	fvmpt	$⊢ y \in B \to (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (y) = if (y \subseteq O (u), F (y), \emptyset)$
366	365	ifeq2d	$⊢ y \in B \to if (y = O (suc u), F (y), (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (y)) = if (y = O (suc u), F (y), if (y \subseteq O (u), F (y), \emptyset))$
367		ifor	$⊢ if ((y = O (suc u) \lor y \subseteq O (u)), F (y), \emptyset) = if (y = O (suc u), F (y), if (y \subseteq O (u), F (y), \emptyset))$
368	366 367	eqtr4di	$⊢ y \in B \to if (y = O (suc u), F (y), (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (y)) = if ((y = O (suc u) \lor y \subseteq O (u)), F (y), \emptyset)$
369	361 368	eqtr3d	$⊢ y \in B \to if (y = O (suc u), F (O (suc u)), (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (y)) = if ((y = O (suc u) \lor y \subseteq O (u)), F (y), \emptyset)$
370	369	mpteq2ia	$⊢ (y \in B ⟼ if (y = O (suc u), F (O (suc u)), (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (y))) = (y \in B ⟼ if ((y = O (suc u) \lor y \subseteq O (u)), F (y), \emptyset))$
371	358 370	eqtr4i	$⊢ (x \in B ⟼ if ((x = O (suc u) \lor x \subseteq O (u)), F (x), \emptyset)) = (y \in B ⟼ if (y = O (suc u), F (O (suc u)), (x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)) (y)))$
372	1 151 148 186 202 208 352 371	cantnfp1	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to ((x \in B ⟼ if ((x = O (suc u) \lor x \subseteq O (u)), F (x), \emptyset)) \in S \land (A CNF B) ((x \in B ⟼ if ((x = O (suc u) \lor x \subseteq O (u)), F (x), \emptyset))) = ((A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u))) +_{𝑜} (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))))$
373	372	simprd	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (A CNF B) ((x \in B ⟼ if ((x = O (suc u) \lor x \subseteq O (u)), F (x), \emptyset))) = ((A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u))) +_{𝑜} (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)))$
374	309 373	eqtrd	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) = ((A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u))) +_{𝑜} (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset)))$
375	1 2 3 9 6 10	cantnfsuc	$⊢ (φ \land suc u \in ω) \to H (suc suc u) = ((A ↑_{𝑜} O (suc u)) \cdot_{𝑜} G (O (suc u))) +_{𝑜} H (suc u)$
376	192 375	syldan	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to H (suc suc u) = ((A ↑_{𝑜} O (suc u)) \cdot_{𝑜} G (O (suc u))) +_{𝑜} H (suc u)$
377	160	simp3d	$⊢ φ \to \forall w \in B (X \in w \to F (w) = G (w))$
378	377	adantr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to \forall w \in B (X \in w \to F (w) = G (w))$
379	109	adantr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O (O^{-1} (X)) = X$
380	136	adantrr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to u \in On$
381		onsssuc	$⊢ (O^{-1} (X) \in On \land u \in On) \to (O^{-1} (X) \subseteq u \leftrightarrow O^{-1} (X) \in suc u)$
382	129 380 381	syl2an2r	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (O^{-1} (X) \subseteq u \leftrightarrow O^{-1} (X) \in suc u)$
383	146 382	mpbid	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O^{-1} (X) \in suc u$
384	53	adantr	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O^{-1} (X) \in dom O$
385		isorel	$⊢ (O {Isom}_{E, E} (dom O, G supp \emptyset) \land (O^{-1} (X) \in dom O \land suc u \in dom O)) \to (O^{-1} (X) E suc u \leftrightarrow O (O^{-1} (X)) E O (suc u))$
386	240 384 143 385	syl12anc	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (O^{-1} (X) E suc u \leftrightarrow O (O^{-1} (X)) E O (suc u))$
387	243	epeli	$⊢ O^{-1} (X) E suc u \leftrightarrow O^{-1} (X) \in suc u$
388	245	epeli	$⊢ O (O^{-1} (X)) E O (suc u) \leftrightarrow O (O^{-1} (X)) \in O (suc u)$
389	386 387 388	3bitr3g	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (O^{-1} (X) \in suc u \leftrightarrow O (O^{-1} (X)) \in O (suc u))$
390	383 389	mpbid	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to O (O^{-1} (X)) \in O (suc u)$
391	379 390	eqeltrrd	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to X \in O (suc u)$
392		eleq2	$⊢ w = O (suc u) \to (X \in w \leftrightarrow X \in O (suc u))$
393		fveq2	$⊢ w = O (suc u) \to F (w) = F (O (suc u))$
394		fveq2	$⊢ w = O (suc u) \to G (w) = G (O (suc u))$
395	393 394	eqeq12d	$⊢ w = O (suc u) \to (F (w) = G (w) \leftrightarrow F (O (suc u)) = G (O (suc u)))$
396	392 395	imbi12d	$⊢ w = O (suc u) \to ((X \in w \to F (w) = G (w)) \leftrightarrow (X \in O (suc u) \to F (O (suc u)) = G (O (suc u))))$
397	396	rspcv	$⊢ O (suc u) \in B \to (\forall w \in B (X \in w \to F (w) = G (w)) \to (X \in O (suc u) \to F (O (suc u)) = G (O (suc u))))$
398	202 378 391 397	syl3c	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to F (O (suc u)) = G (O (suc u))$
399	398	oveq2d	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u)) = (A ↑_{𝑜} O (suc u)) \cdot_{𝑜} G (O (suc u))$
400	399	oveq1d	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to ((A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u))) +_{𝑜} H (suc u) = ((A ↑_{𝑜} O (suc u)) \cdot_{𝑜} G (O (suc u))) +_{𝑜} H (suc u)$
401	376 400	eqtr4d	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to H (suc suc u) = ((A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u))) +_{𝑜} H (suc u)$
402	374 401	eleq12d	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to ((A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u) \leftrightarrow ((A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u))) +_{𝑜} (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in (((A ↑_{𝑜} O (suc u)) \cdot_{𝑜} F (O (suc u))) +_{𝑜} H (suc u)))$
403	214 402	bitr4d	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to ((A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u) \leftrightarrow (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u))$
404	403	biimpd	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to ((A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u))$
405	147 404	embantd	$⊢ (φ \land (suc u \in dom O \land O^{-1} (X) \subseteq u)) \to (((u \in dom O \land O^{-1} (X) \subseteq u) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u)) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u))$
406	405	expr	$⊢ (φ \land suc u \in dom O) \to (O^{-1} (X) \subseteq u \to (((u \in dom O \land O^{-1} (X) \subseteq u) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u)) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u)))$
407	140 406	sylbird	$⊢ (φ \land suc u \in dom O) \to (O^{-1} (X) \in suc u \to (((u \in dom O \land O^{-1} (X) \subseteq u) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u)) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u)))$
408		fveq2	$⊢ O^{-1} (X) = suc u \to O (O^{-1} (X)) = O (suc u)$
409	408	sseq2d	$⊢ O^{-1} (X) = suc u \to (x \subseteq O (O^{-1} (X)) \leftrightarrow x \subseteq O (suc u))$
410	409	ifbid	$⊢ O^{-1} (X) = suc u \to if (x \subseteq O (O^{-1} (X)), F (x), \emptyset) = if (x \subseteq O (suc u), F (x), \emptyset)$
411	410	mpteq2dv	$⊢ O^{-1} (X) = suc u \to (x \in B ⟼ if (x \subseteq O (O^{-1} (X)), F (x), \emptyset)) = (x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))$
412	411	fveq2d	$⊢ O^{-1} (X) = suc u \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (O^{-1} (X)), F (x), \emptyset))) = (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset)))$
413		suceq	$⊢ O^{-1} (X) = suc u \to suc O^{-1} (X) = suc suc u$
414	413	fveq2d	$⊢ O^{-1} (X) = suc u \to H (suc O^{-1} (X)) = H (suc suc u)$
415	412 414	eleq12d	$⊢ O^{-1} (X) = suc u \to ((A CNF B) ((x \in B ⟼ if (x \subseteq O (O^{-1} (X)), F (x), \emptyset))) \in H (suc O^{-1} (X)) \leftrightarrow (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u))$
416	115 415	syl5ibcom	$⊢ φ \to (O^{-1} (X) = suc u \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u))$
417	416	adantr	$⊢ (φ \land suc u \in dom O) \to (O^{-1} (X) = suc u \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u))$
418	417	a1dd	$⊢ (φ \land suc u \in dom O) \to (O^{-1} (X) = suc u \to (((u \in dom O \land O^{-1} (X) \subseteq u) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u)) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u)))$
419	407 418	jaod	$⊢ (φ \land suc u \in dom O) \to ((O^{-1} (X) \in suc u \lor O^{-1} (X) = suc u) \to (((u \in dom O \land O^{-1} (X) \subseteq u) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u)) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u)))$
420	134 419	sylbid	$⊢ (φ \land suc u \in dom O) \to (O^{-1} (X) \subseteq suc u \to (((u \in dom O \land O^{-1} (X) \subseteq u) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u)) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u)))$
421	420	expimpd	$⊢ φ \to ((suc u \in dom O \land O^{-1} (X) \subseteq suc u) \to (((u \in dom O \land O^{-1} (X) \subseteq u) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u)) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u)))$
422	421	com23	$⊢ φ \to (((u \in dom O \land O^{-1} (X) \subseteq u) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u)) \to ((suc u \in dom O \land O^{-1} (X) \subseteq suc u) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u)))$
423	422	a1i	$⊢ u \in ω \to (φ \to (((u \in dom O \land O^{-1} (X) \subseteq u) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (u), F (x), \emptyset))) \in H (suc u)) \to ((suc u \in dom O \land O^{-1} (X) \subseteq suc u) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (suc u), F (x), \emptyset))) \in H (suc suc u))))$
424	83 95 107 127 423	finds2	$⊢ y \in ω \to (φ \to ((y \in dom O \land O^{-1} (X) \subseteq y) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (y), F (x), \emptyset))) \in H (suc y)))$
425	71 424	vtoclga	$⊢ ⋃ dom O \in ω \to (φ \to ((⋃ dom O \in dom O \land O^{-1} (X) \subseteq ⋃ dom O) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (⋃ dom O), F (x), \emptyset))) \in H (suc ⋃ dom O)))$
426	58 425	mpcom	$⊢ φ \to ((⋃ dom O \in dom O \land O^{-1} (X) \subseteq ⋃ dom O) \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (⋃ dom O), F (x), \emptyset))) \in H (suc ⋃ dom O))$
427	45 55 426	mp2and	$⊢ φ \to (A CNF B) ((x \in B ⟼ if (x \subseteq O (⋃ dom O), F (x), \emptyset))) \in H (suc ⋃ dom O)$
428	155	feqmptd	$⊢ φ \to F = (x \in B ⟼ F (x))$
429		eqeq2	$⊢ F (x) = if (x \subseteq O (⋃ dom O), F (x), \emptyset) \to (F (x) = F (x) \leftrightarrow F (x) = if (x \subseteq O (⋃ dom O), F (x), \emptyset))$
430		eqeq2	$⊢ \emptyset = if (x \subseteq O (⋃ dom O), F (x), \emptyset) \to (F (x) = \emptyset \leftrightarrow F (x) = if (x \subseteq O (⋃ dom O), F (x), \emptyset))$
431		eqidd	$⊢ ((φ \land x \in B) \land x \subseteq O (⋃ dom O)) \to F (x) = F (x)$
432	199	ffvelcdmi	$⊢ ⋃ dom O \in dom O \to O (⋃ dom O) \in {supp}_{\emptyset} (G)$
433	45 432	syl	$⊢ φ \to O (⋃ dom O) \in {supp}_{\emptyset} (G)$
434	197 433	sseldd	$⊢ φ \to O (⋃ dom O) \in B$
435		onelon	$⊢ (B \in On \land O (⋃ dom O) \in B) \to O (⋃ dom O) \in On$
436	3 434 435	syl2anc	$⊢ φ \to O (⋃ dom O) \in On$
437	436	adantr	$⊢ (φ \land x \in B) \to O (⋃ dom O) \in On$
438		ontri1	$⊢ (x \in On \land O (⋃ dom O) \in On) \to (x \subseteq O (⋃ dom O) \leftrightarrow \neg O (⋃ dom O) \in x)$
439	224 437 438	syl2anc	$⊢ (φ \land x \in B) \to (x \subseteq O (⋃ dom O) \leftrightarrow \neg O (⋃ dom O) \in x)$
440	439	con2bid	$⊢ (φ \land x \in B) \to (O (⋃ dom O) \in x \leftrightarrow \neg x \subseteq O (⋃ dom O))$
441		simprl	$⊢ (φ \land (x \in B \land O (⋃ dom O) \in x)) \to x \in B$
442	377	adantr	$⊢ (φ \land (x \in B \land O (⋃ dom O) \in x)) \to \forall w \in B (X \in w \to F (w) = G (w))$
443		eloni	$⊢ O^{-1} (X) \in On \to Ord O^{-1} (X)$
444	129 443	syl	$⊢ φ \to Ord O^{-1} (X)$
445		orduni	$⊢ Ord dom O \to Ord ⋃ dom O$
446	37 445	ax-mp	$⊢ Ord ⋃ dom O$
447		ordtri1	$⊢ (Ord O^{-1} (X) \land Ord ⋃ dom O) \to (O^{-1} (X) \subseteq ⋃ dom O \leftrightarrow \neg ⋃ dom O \in O^{-1} (X))$
448	444 446 447	sylancl	$⊢ φ \to (O^{-1} (X) \subseteq ⋃ dom O \leftrightarrow \neg ⋃ dom O \in O^{-1} (X))$
449	55 448	mpbid	$⊢ φ \to \neg ⋃ dom O \in O^{-1} (X)$
450		isorel	$⊢ (O {Isom}_{E, E} (dom O, G supp \emptyset) \land (⋃ dom O \in dom O \land O^{-1} (X) \in dom O)) \to (⋃ dom O E O^{-1} (X) \leftrightarrow O (⋃ dom O) E O (O^{-1} (X)))$
451	47 45 53 450	syl12anc	$⊢ φ \to (⋃ dom O E O^{-1} (X) \leftrightarrow O (⋃ dom O) E O (O^{-1} (X)))$
452		fvex	$⊢ O^{-1} (X) \in V$
453	452	epeli	$⊢ ⋃ dom O E O^{-1} (X) \leftrightarrow ⋃ dom O \in O^{-1} (X)$
454		fvex	$⊢ O (O^{-1} (X)) \in V$
455	454	epeli	$⊢ O (⋃ dom O) E O (O^{-1} (X)) \leftrightarrow O (⋃ dom O) \in O (O^{-1} (X))$
456	451 453 455	3bitr3g	$⊢ φ \to (⋃ dom O \in O^{-1} (X) \leftrightarrow O (⋃ dom O) \in O (O^{-1} (X)))$
457	109	eleq2d	$⊢ φ \to (O (⋃ dom O) \in O (O^{-1} (X)) \leftrightarrow O (⋃ dom O) \in X)$
458	456 457	bitrd	$⊢ φ \to (⋃ dom O \in O^{-1} (X) \leftrightarrow O (⋃ dom O) \in X)$
459	449 458	mtbid	$⊢ φ \to \neg O (⋃ dom O) \in X$
460		onelon	$⊢ (B \in On \land X \in B) \to X \in On$
461	3 161 460	syl2anc	$⊢ φ \to X \in On$
462		ontri1	$⊢ (X \in On \land O (⋃ dom O) \in On) \to (X \subseteq O (⋃ dom O) \leftrightarrow \neg O (⋃ dom O) \in X)$
463	461 436 462	syl2anc	$⊢ φ \to (X \subseteq O (⋃ dom O) \leftrightarrow \neg O (⋃ dom O) \in X)$
464	459 463	mpbird	$⊢ φ \to X \subseteq O (⋃ dom O)$
465	464	adantr	$⊢ (φ \land (x \in B \land O (⋃ dom O) \in x)) \to X \subseteq O (⋃ dom O)$
466		simprr	$⊢ (φ \land (x \in B \land O (⋃ dom O) \in x)) \to O (⋃ dom O) \in x$
467	224	adantrr	$⊢ (φ \land (x \in B \land O (⋃ dom O) \in x)) \to x \in On$
468		ontr2	$⊢ (X \in On \land x \in On) \to ((X \subseteq O (⋃ dom O) \land O (⋃ dom O) \in x) \to X \in x)$
469	461 467 468	syl2an2r	$⊢ (φ \land (x \in B \land O (⋃ dom O) \in x)) \to ((X \subseteq O (⋃ dom O) \land O (⋃ dom O) \in x) \to X \in x)$
470	465 466 469	mp2and	$⊢ (φ \land (x \in B \land O (⋃ dom O) \in x)) \to X \in x$
471		eleq2	$⊢ w = x \to (X \in w \leftrightarrow X \in x)$
472		fveq2	$⊢ w = x \to F (w) = F (x)$
473		fveq2	$⊢ w = x \to G (w) = G (x)$
474	472 473	eqeq12d	$⊢ w = x \to (F (w) = G (w) \leftrightarrow F (x) = G (x))$
475	471 474	imbi12d	$⊢ w = x \to ((X \in w \to F (w) = G (w)) \leftrightarrow (X \in x \to F (x) = G (x)))$
476	475	rspcv	$⊢ x \in B \to (\forall w \in B (X \in w \to F (w) = G (w)) \to (X \in x \to F (x) = G (x)))$
477	441 442 470 476	syl3c	$⊢ (φ \land (x \in B \land O (⋃ dom O) \in x)) \to F (x) = G (x)$
478	466	adantr	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to O (⋃ dom O) \in x$
479	47	ad2antrr	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to O {Isom}_{E, E} (dom O, G supp \emptyset)$
480	45	ad2antrr	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to ⋃ dom O \in dom O$
481	52	ad2antrr	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to O^{-1} : G supp \emptyset ⟶ dom O$
482		ffvelcdm	$⊢ (O^{-1} : G supp \emptyset ⟶ dom O \land x \in {supp}_{\emptyset} (G)) \to O^{-1} (x) \in dom O$
483	481 482	sylancom	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to O^{-1} (x) \in dom O$
484		isorel	$⊢ (O {Isom}_{E, E} (dom O, G supp \emptyset) \land (⋃ dom O \in dom O \land O^{-1} (x) \in dom O)) \to (⋃ dom O E O^{-1} (x) \leftrightarrow O (⋃ dom O) E O (O^{-1} (x)))$
485	479 480 483 484	syl12anc	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to (⋃ dom O E O^{-1} (x) \leftrightarrow O (⋃ dom O) E O (O^{-1} (x)))$
486	269	epeli	$⊢ ⋃ dom O E O^{-1} (x) \leftrightarrow ⋃ dom O \in O^{-1} (x)$
487	271	epeli	$⊢ O (⋃ dom O) E O (O^{-1} (x)) \leftrightarrow O (⋃ dom O) \in O (O^{-1} (x))$
488	485 486 487	3bitr3g	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to (⋃ dom O \in O^{-1} (x) \leftrightarrow O (⋃ dom O) \in O (O^{-1} (x)))$
489	49	ad2antrr	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to O : dom O \underset{1-1 onto}{⟶} G supp \emptyset$
490	489 261	sylancom	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to O (O^{-1} (x)) = x$
491	490	eleq2d	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to (O (⋃ dom O) \in O (O^{-1} (x)) \leftrightarrow O (⋃ dom O) \in x)$
492	488 491	bitrd	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to (⋃ dom O \in O^{-1} (x) \leftrightarrow O (⋃ dom O) \in x)$
493	478 492	mpbird	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to ⋃ dom O \in O^{-1} (x)$
494		elssuni	$⊢ O^{-1} (x) \in dom O \to O^{-1} (x) \subseteq ⋃ dom O$
495	483 494	syl	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to O^{-1} (x) \subseteq ⋃ dom O$
496	37 483 275	sylancr	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to O^{-1} (x) \in On$
497	496 277	syl	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to Ord O^{-1} (x)$
498		ordtri1	$⊢ (Ord O^{-1} (x) \land Ord ⋃ dom O) \to (O^{-1} (x) \subseteq ⋃ dom O \leftrightarrow \neg ⋃ dom O \in O^{-1} (x))$
499	497 446 498	sylancl	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to (O^{-1} (x) \subseteq ⋃ dom O \leftrightarrow \neg ⋃ dom O \in O^{-1} (x))$
500	495 499	mpbid	$⊢ ((φ \land (x \in B \land O (⋃ dom O) \in x)) \land x \in {supp}_{\emptyset} (G)) \to \neg ⋃ dom O \in O^{-1} (x)$
501	493 500	pm2.65da	$⊢ (φ \land (x \in B \land O (⋃ dom O) \in x)) \to \neg x \in {supp}_{\emptyset} (G)$
502	441 501	eldifd	$⊢ (φ \land (x \in B \land O (⋃ dom O) \in x)) \to x \in (B ∖ {supp}_{\emptyset} (G))$
503		ssidd	$⊢ φ \to G supp \emptyset \subseteq G supp \emptyset$
504	159 503 3 176	suppssr	$⊢ (φ \land x \in (B ∖ {supp}_{\emptyset} (G))) \to G (x) = \emptyset$
505	502 504	syldan	$⊢ (φ \land (x \in B \land O (⋃ dom O) \in x)) \to G (x) = \emptyset$
506	477 505	eqtrd	$⊢ (φ \land (x \in B \land O (⋃ dom O) \in x)) \to F (x) = \emptyset$
507	506	expr	$⊢ (φ \land x \in B) \to (O (⋃ dom O) \in x \to F (x) = \emptyset)$
508	440 507	sylbird	$⊢ (φ \land x \in B) \to (\neg x \subseteq O (⋃ dom O) \to F (x) = \emptyset)$
509	508	imp	$⊢ ((φ \land x \in B) \land \neg x \subseteq O (⋃ dom O)) \to F (x) = \emptyset$
510	429 430 431 509	ifbothda	$⊢ (φ \land x \in B) \to F (x) = if (x \subseteq O (⋃ dom O), F (x), \emptyset)$
511	510	mpteq2dva	$⊢ φ \to (x \in B ⟼ F (x)) = (x \in B ⟼ if (x \subseteq O (⋃ dom O), F (x), \emptyset))$
512	428 511	eqtrd	$⊢ φ \to F = (x \in B ⟼ if (x \subseteq O (⋃ dom O), F (x), \emptyset))$
513	512	fveq2d	$⊢ φ \to (A CNF B) (F) = (A CNF B) ((x \in B ⟼ if (x \subseteq O (⋃ dom O), F (x), \emptyset)))$
514	1 2 3 9 6 10	cantnfval	$⊢ φ \to (A CNF B) (G) = H (dom O)$
515	44	fveq2d	$⊢ φ \to H (dom O) = H (suc ⋃ dom O)$
516	514 515	eqtrd	$⊢ φ \to (A CNF B) (G) = H (suc ⋃ dom O)$
517	427 513 516	3eltr4d	$⊢ φ \to (A CNF B) (F) \in (A CNF B) (G)$

Metamath Proof Explorer

Theorem cantnflem1

Proof