cantnfp1lem3

Description: Lemma for cantnfp1 . (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 1-Jul-2019)

	Ref	Expression
Hypotheses	cantnfs.s	$⊢ S = dom (A CNF B)$
	cantnfs.a	$⊢ φ \to A \in On$
	cantnfs.b	$⊢ φ \to B \in On$
	cantnfp1.g	$⊢ φ \to G \in S$
	cantnfp1.x	$⊢ φ \to X \in B$
	cantnfp1.y	$⊢ φ \to Y \in A$
	cantnfp1.s	$⊢ φ \to G supp \emptyset \subseteq X$
	cantnfp1.f	$⊢ F = (t \in B ⟼ if (t = X, Y, G (t)))$
	cantnfp1.e	$⊢ φ \to \emptyset \in Y$
	cantnfp1.o	$⊢ O = OrdIso (E, F supp \emptyset)$
	cantnfp1.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} O (k)) \cdot_{𝑜} F (O (k))) +_{𝑜} z), \emptyset)$
	cantnfp1.k	$⊢ K = OrdIso (E, G supp \emptyset)$
	cantnfp1.m	$⊢ M = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} K (k)) \cdot_{𝑜} G (K (k))) +_{𝑜} z), \emptyset)$
Assertion	cantnfp1lem3	$⊢ φ \to (A CNF B) (F) = ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} (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		cantnfp1.g	$⊢ φ \to G \in S$
5		cantnfp1.x	$⊢ φ \to X \in B$
6		cantnfp1.y	$⊢ φ \to Y \in A$
7		cantnfp1.s	$⊢ φ \to G supp \emptyset \subseteq X$
8		cantnfp1.f	$⊢ F = (t \in B ⟼ if (t = X, Y, G (t)))$
9		cantnfp1.e	$⊢ φ \to \emptyset \in Y$
10		cantnfp1.o	$⊢ O = OrdIso (E, F supp \emptyset)$
11		cantnfp1.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} O (k)) \cdot_{𝑜} F (O (k))) +_{𝑜} z), \emptyset)$
12		cantnfp1.k	$⊢ K = OrdIso (E, G supp \emptyset)$
13		cantnfp1.m	$⊢ M = {seq}_{ω} ((k \in V, z \in V ⟼ ((A ↑_{𝑜} K (k)) \cdot_{𝑜} G (K (k))) +_{𝑜} z), \emptyset)$
14	1 2 3 4 5 6 7 8	cantnfp1lem1	$⊢ φ \to F \in S$
15	1 2 3 10 14 11	cantnfval	$⊢ φ \to (A CNF B) (F) = H (dom O)$
16	1 2 3 4 5 6 7 8 9 10	cantnfp1lem2	$⊢ φ \to dom O = suc ⋃ dom O$
17	16	fveq2d	$⊢ φ \to H (dom O) = H (suc ⋃ dom O)$
18	1 2 3 10 14	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (F) \land dom O \in ω)$
19	18	simprd	$⊢ φ \to dom O \in ω$
20	16 19	eqeltrrd	$⊢ φ \to suc ⋃ dom O \in ω$
21		peano2b	$⊢ ⋃ dom O \in ω \leftrightarrow suc ⋃ dom O \in ω$
22	20 21	sylibr	$⊢ φ \to ⋃ dom O \in ω$
23	1 2 3 10 14 11	cantnfsuc	$⊢ (φ \land ⋃ dom O \in ω) \to H (suc ⋃ dom O) = ((A ↑_{𝑜} O (⋃ dom O)) \cdot_{𝑜} F (O (⋃ dom O))) +_{𝑜} H (⋃ dom O)$
24	22 23	mpdan	$⊢ φ \to H (suc ⋃ dom O) = ((A ↑_{𝑜} O (⋃ dom O)) \cdot_{𝑜} F (O (⋃ dom O))) +_{𝑜} H (⋃ dom O)$
25		ovexd	$⊢ φ \to F supp \emptyset \in V$
26	18	simpld	$⊢ φ \to E We {supp}_{\emptyset} (F)$
27	10	oiiso	$⊢ (F supp \emptyset \in V \land E We {supp}_{\emptyset} (F)) \to O {Isom}_{E, E} (dom O, F supp \emptyset)$
28	25 26 27	syl2anc	$⊢ φ \to O {Isom}_{E, E} (dom O, F supp \emptyset)$
29		isof1o	$⊢ O {Isom}_{E, E} (dom O, F supp \emptyset) \to O : dom O \underset{1-1 onto}{⟶} F supp \emptyset$
30	28 29	syl	$⊢ φ \to O : dom O \underset{1-1 onto}{⟶} F supp \emptyset$
31		f1ocnv	$⊢ O : dom O \underset{1-1 onto}{⟶} F supp \emptyset \to O^{-1} : F supp \emptyset \underset{1-1 onto}{⟶} dom O$
32		f1of	$⊢ O^{-1} : F supp \emptyset \underset{1-1 onto}{⟶} dom O \to O^{-1} : F supp \emptyset ⟶ dom O$
33	30 31 32	3syl	$⊢ φ \to O^{-1} : F supp \emptyset ⟶ dom O$
34		iftrue	$⊢ t = X \to if (t = X, Y, G (t)) = Y$
35	8 34 5 6	fvmptd3	$⊢ φ \to F (X) = Y$
36	9	ne0d	$⊢ φ \to Y \neq \emptyset$
37	35 36	eqnetrd	$⊢ φ \to F (X) \neq \emptyset$
38	6	adantr	$⊢ (φ \land t \in B) \to Y \in A$
39	1 2 3	cantnfs	$⊢ φ \to (G \in S \leftrightarrow (G : B ⟶ A \land {finSupp}_{\emptyset} (G)))$
40	4 39	mpbid	$⊢ φ \to (G : B ⟶ A \land {finSupp}_{\emptyset} (G))$
41	40	simpld	$⊢ φ \to G : B ⟶ A$
42	41	ffvelcdmda	$⊢ (φ \land t \in B) \to G (t) \in A$
43	38 42	ifcld	$⊢ (φ \land t \in B) \to if (t = X, Y, G (t)) \in A$
44	43 8	fmptd	$⊢ φ \to F : B ⟶ A$
45	44	ffnd	$⊢ φ \to F Fn B$
46		0ex	$⊢ \emptyset \in V$
47	46	a1i	$⊢ φ \to \emptyset \in V$
48		elsuppfn	$⊢ (F Fn B \land B \in On \land \emptyset \in V) \to (X \in {supp}_{\emptyset} (F) \leftrightarrow (X \in B \land F (X) \neq \emptyset))$
49	45 3 47 48	syl3anc	$⊢ φ \to (X \in {supp}_{\emptyset} (F) \leftrightarrow (X \in B \land F (X) \neq \emptyset))$
50	5 37 49	mpbir2and	$⊢ φ \to X \in {supp}_{\emptyset} (F)$
51	33 50	ffvelcdmd	$⊢ φ \to O^{-1} (X) \in dom O$
52		elssuni	$⊢ O^{-1} (X) \in dom O \to O^{-1} (X) \subseteq ⋃ dom O$
53	51 52	syl	$⊢ φ \to O^{-1} (X) \subseteq ⋃ dom O$
54	10	oicl	$⊢ Ord dom O$
55		ordelon	$⊢ (Ord dom O \land O^{-1} (X) \in dom O) \to O^{-1} (X) \in On$
56	54 51 55	sylancr	$⊢ φ \to O^{-1} (X) \in On$
57		nnon	$⊢ ⋃ dom O \in ω \to ⋃ dom O \in On$
58	22 57	syl	$⊢ φ \to ⋃ dom O \in On$
59		ontri1	$⊢ (O^{-1} (X) \in On \land ⋃ dom O \in On) \to (O^{-1} (X) \subseteq ⋃ dom O \leftrightarrow \neg ⋃ dom O \in O^{-1} (X))$
60	56 58 59	syl2anc	$⊢ φ \to (O^{-1} (X) \subseteq ⋃ dom O \leftrightarrow \neg ⋃ dom O \in O^{-1} (X))$
61	53 60	mpbid	$⊢ φ \to \neg ⋃ dom O \in O^{-1} (X)$
62		sucidg	$⊢ ⋃ dom O \in ω \to ⋃ dom O \in suc ⋃ dom O$
63	22 62	syl	$⊢ φ \to ⋃ dom O \in suc ⋃ dom O$
64	63 16	eleqtrrd	$⊢ φ \to ⋃ dom O \in dom O$
65		isorel	$⊢ (O {Isom}_{E, E} (dom O, F 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)))$
66	28 64 51 65	syl12anc	$⊢ φ \to (⋃ dom O E O^{-1} (X) \leftrightarrow O (⋃ dom O) E O (O^{-1} (X)))$
67		fvex	$⊢ O^{-1} (X) \in V$
68	67	epeli	$⊢ ⋃ dom O E O^{-1} (X) \leftrightarrow ⋃ dom O \in O^{-1} (X)$
69		fvex	$⊢ O (O^{-1} (X)) \in V$
70	69	epeli	$⊢ O (⋃ dom O) E O (O^{-1} (X)) \leftrightarrow O (⋃ dom O) \in O (O^{-1} (X))$
71	66 68 70	3bitr3g	$⊢ φ \to (⋃ dom O \in O^{-1} (X) \leftrightarrow O (⋃ dom O) \in O (O^{-1} (X)))$
72		f1ocnvfv2	$⊢ (O : dom O \underset{1-1 onto}{⟶} F supp \emptyset \land X \in {supp}_{\emptyset} (F)) \to O (O^{-1} (X)) = X$
73	30 50 72	syl2anc	$⊢ φ \to O (O^{-1} (X)) = X$
74	73	eleq2d	$⊢ φ \to (O (⋃ dom O) \in O (O^{-1} (X)) \leftrightarrow O (⋃ dom O) \in X)$
75	71 74	bitrd	$⊢ φ \to (⋃ dom O \in O^{-1} (X) \leftrightarrow O (⋃ dom O) \in X)$
76	61 75	mtbid	$⊢ φ \to \neg O (⋃ dom O) \in X$
77	7	sseld	$⊢ φ \to (O (⋃ dom O) \in {supp}_{\emptyset} (G) \to O (⋃ dom O) \in X)$
78		suppssdm	$⊢ F supp \emptyset \subseteq dom F$
79	78 44	fssdm	$⊢ φ \to F supp \emptyset \subseteq B$
80		onss	$⊢ B \in On \to B \subseteq On$
81	3 80	syl	$⊢ φ \to B \subseteq On$
82	79 81	sstrd	$⊢ φ \to F supp \emptyset \subseteq On$
83	10	oif	$⊢ O : dom O ⟶ F supp \emptyset$
84	83	ffvelcdmi	$⊢ ⋃ dom O \in dom O \to O (⋃ dom O) \in {supp}_{\emptyset} (F)$
85	64 84	syl	$⊢ φ \to O (⋃ dom O) \in {supp}_{\emptyset} (F)$
86	82 85	sseldd	$⊢ φ \to O (⋃ dom O) \in On$
87		eloni	$⊢ O (⋃ dom O) \in On \to Ord O (⋃ dom O)$
88	86 87	syl	$⊢ φ \to Ord O (⋃ dom O)$
89		ordn2lp	$⊢ Ord O (⋃ dom O) \to \neg (O (⋃ dom O) \in X \land X \in O (⋃ dom O))$
90	88 89	syl	$⊢ φ \to \neg (O (⋃ dom O) \in X \land X \in O (⋃ dom O))$
91		imnan	$⊢ (O (⋃ dom O) \in X \to \neg X \in O (⋃ dom O)) \leftrightarrow \neg (O (⋃ dom O) \in X \land X \in O (⋃ dom O))$
92	90 91	sylibr	$⊢ φ \to (O (⋃ dom O) \in X \to \neg X \in O (⋃ dom O))$
93	77 92	syld	$⊢ φ \to (O (⋃ dom O) \in {supp}_{\emptyset} (G) \to \neg X \in O (⋃ dom O))$
94		onelon	$⊢ (B \in On \land X \in B) \to X \in On$
95	3 5 94	syl2anc	$⊢ φ \to X \in On$
96		eloni	$⊢ X \in On \to Ord X$
97	95 96	syl	$⊢ φ \to Ord X$
98		ordirr	$⊢ Ord X \to \neg X \in X$
99	97 98	syl	$⊢ φ \to \neg X \in X$
100		elsni	$⊢ O (⋃ dom O) \in \{X\} \to O (⋃ dom O) = X$
101	100	eleq2d	$⊢ O (⋃ dom O) \in \{X\} \to (X \in O (⋃ dom O) \leftrightarrow X \in X)$
102	101	notbid	$⊢ O (⋃ dom O) \in \{X\} \to (\neg X \in O (⋃ dom O) \leftrightarrow \neg X \in X)$
103	99 102	syl5ibrcom	$⊢ φ \to (O (⋃ dom O) \in \{X\} \to \neg X \in O (⋃ dom O))$
104		eqeq1	$⊢ t = k \to (t = X \leftrightarrow k = X)$
105		fveq2	$⊢ t = k \to G (t) = G (k)$
106	104 105	ifbieq2d	$⊢ t = k \to if (t = X, Y, G (t)) = if (k = X, Y, G (k))$
107		eldifi	$⊢ k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\})) \to k \in B$
108	107	adantl	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to k \in B$
109	6	adantr	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to Y \in A$
110		fvex	$⊢ G (k) \in V$
111		ifexg	$⊢ (Y \in A \land G (k) \in V) \to if (k = X, Y, G (k)) \in V$
112	109 110 111	sylancl	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to if (k = X, Y, G (k)) \in V$
113	8 106 108 112	fvmptd3	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to F (k) = if (k = X, Y, G (k))$
114		eldifn	$⊢ k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\})) \to \neg k \in ({supp}_{\emptyset} (G) \cup \{X\})$
115	114	adantl	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to \neg k \in ({supp}_{\emptyset} (G) \cup \{X\})$
116		velsn	$⊢ k \in \{X\} \leftrightarrow k = X$
117		elun2	$⊢ k \in \{X\} \to k \in ({supp}_{\emptyset} (G) \cup \{X\})$
118	116 117	sylbir	$⊢ k = X \to k \in ({supp}_{\emptyset} (G) \cup \{X\})$
119	115 118	nsyl	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to \neg k = X$
120	119	iffalsed	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to if (k = X, Y, G (k)) = G (k)$
121		ssun1	$⊢ G supp \emptyset \subseteq {supp}_{\emptyset} (G) \cup \{X\}$
122		sscon	$⊢ G supp \emptyset \subseteq {supp}_{\emptyset} (G) \cup \{X\} \to B ∖ ({supp}_{\emptyset} (G) \cup \{X\}) \subseteq B ∖ {supp}_{\emptyset} (G)$
123	121 122	ax-mp	$⊢ B ∖ ({supp}_{\emptyset} (G) \cup \{X\}) \subseteq B ∖ {supp}_{\emptyset} (G)$
124	123	sseli	$⊢ k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\})) \to k \in (B ∖ {supp}_{\emptyset} (G))$
125		ssidd	$⊢ φ \to G supp \emptyset \subseteq G supp \emptyset$
126	41 125 3 9	suppssr	$⊢ (φ \land k \in (B ∖ {supp}_{\emptyset} (G))) \to G (k) = \emptyset$
127	124 126	sylan2	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to G (k) = \emptyset$
128	113 120 127	3eqtrd	$⊢ (φ \land k \in (B ∖ ({supp}_{\emptyset} (G) \cup \{X\}))) \to F (k) = \emptyset$
129	44 128	suppss	$⊢ φ \to F supp \emptyset \subseteq {supp}_{\emptyset} (G) \cup \{X\}$
130	129 85	sseldd	$⊢ φ \to O (⋃ dom O) \in ({supp}_{\emptyset} (G) \cup \{X\})$
131		elun	$⊢ O (⋃ dom O) \in ({supp}_{\emptyset} (G) \cup \{X\}) \leftrightarrow (O (⋃ dom O) \in {supp}_{\emptyset} (G) \lor O (⋃ dom O) \in \{X\})$
132	130 131	sylib	$⊢ φ \to (O (⋃ dom O) \in {supp}_{\emptyset} (G) \lor O (⋃ dom O) \in \{X\})$
133	93 103 132	mpjaod	$⊢ φ \to \neg X \in O (⋃ dom O)$
134		ioran	$⊢ \neg (O (⋃ dom O) \in X \lor X \in O (⋃ dom O)) \leftrightarrow (\neg O (⋃ dom O) \in X \land \neg X \in O (⋃ dom O))$
135	76 133 134	sylanbrc	$⊢ φ \to \neg (O (⋃ dom O) \in X \lor X \in O (⋃ dom O))$
136		ordtri3	$⊢ (Ord O (⋃ dom O) \land Ord X) \to (O (⋃ dom O) = X \leftrightarrow \neg (O (⋃ dom O) \in X \lor X \in O (⋃ dom O)))$
137	88 97 136	syl2anc	$⊢ φ \to (O (⋃ dom O) = X \leftrightarrow \neg (O (⋃ dom O) \in X \lor X \in O (⋃ dom O)))$
138	135 137	mpbird	$⊢ φ \to O (⋃ dom O) = X$
139	138	oveq2d	$⊢ φ \to A ↑_{𝑜} O (⋃ dom O) = A ↑_{𝑜} X$
140	138	fveq2d	$⊢ φ \to F (O (⋃ dom O)) = F (X)$
141	140 35	eqtrd	$⊢ φ \to F (O (⋃ dom O)) = Y$
142	139 141	oveq12d	$⊢ φ \to (A ↑_{𝑜} O (⋃ dom O)) \cdot_{𝑜} F (O (⋃ dom O)) = (A ↑_{𝑜} X) \cdot_{𝑜} Y$
143		nnord	$⊢ ⋃ dom O \in ω \to Ord ⋃ dom O$
144	22 143	syl	$⊢ φ \to Ord ⋃ dom O$
145		sssucid	$⊢ ⋃ dom O \subseteq suc ⋃ dom O$
146	145 16	sseqtrrid	$⊢ φ \to ⋃ dom O \subseteq dom O$
147		f1ofo	$⊢ O : dom O \underset{1-1 onto}{⟶} F supp \emptyset \to O : dom O \underset{onto}{⟶} F supp \emptyset$
148	30 147	syl	$⊢ φ \to O : dom O \underset{onto}{⟶} F supp \emptyset$
149		foima	$⊢ O : dom O \underset{onto}{⟶} F supp \emptyset \to O [dom O] = F supp \emptyset$
150	148 149	syl	$⊢ φ \to O [dom O] = F supp \emptyset$
151		ffn	$⊢ O : dom O ⟶ F supp \emptyset \to O Fn dom O$
152	83 151	ax-mp	$⊢ O Fn dom O$
153		fnsnfv	$⊢ (O Fn dom O \land ⋃ dom O \in dom O) \to \{O (⋃ dom O)\} = O [\{⋃ dom O\}]$
154	152 64 153	sylancr	$⊢ φ \to \{O (⋃ dom O)\} = O [\{⋃ dom O\}]$
155	138	sneqd	$⊢ φ \to \{O (⋃ dom O)\} = \{X\}$
156	154 155	eqtr3d	$⊢ φ \to O [\{⋃ dom O\}] = \{X\}$
157	150 156	difeq12d	$⊢ φ \to O [dom O] ∖ O [\{⋃ dom O\}] = {supp}_{\emptyset} (F) ∖ \{X\}$
158		ordirr	$⊢ Ord ⋃ dom O \to \neg ⋃ dom O \in ⋃ dom O$
159	144 158	syl	$⊢ φ \to \neg ⋃ dom O \in ⋃ dom O$
160		disjsn	$⊢ ⋃ dom O \cap \{⋃ dom O\} = \emptyset \leftrightarrow \neg ⋃ dom O \in ⋃ dom O$
161	159 160	sylibr	$⊢ φ \to ⋃ dom O \cap \{⋃ dom O\} = \emptyset$
162		disj3	$⊢ ⋃ dom O \cap \{⋃ dom O\} = \emptyset \leftrightarrow ⋃ dom O = ⋃ dom O ∖ \{⋃ dom O\}$
163	161 162	sylib	$⊢ φ \to ⋃ dom O = ⋃ dom O ∖ \{⋃ dom O\}$
164		difun2	$⊢ (⋃ dom O \cup \{⋃ dom O\}) ∖ \{⋃ dom O\} = ⋃ dom O ∖ \{⋃ dom O\}$
165	163 164	eqtr4di	$⊢ φ \to ⋃ dom O = (⋃ dom O \cup \{⋃ dom O\}) ∖ \{⋃ dom O\}$
166		df-suc	$⊢ suc ⋃ dom O = ⋃ dom O \cup \{⋃ dom O\}$
167	16 166	eqtrdi	$⊢ φ \to dom O = ⋃ dom O \cup \{⋃ dom O\}$
168	167	difeq1d	$⊢ φ \to dom O ∖ \{⋃ dom O\} = (⋃ dom O \cup \{⋃ dom O\}) ∖ \{⋃ dom O\}$
169	165 168	eqtr4d	$⊢ φ \to ⋃ dom O = dom O ∖ \{⋃ dom O\}$
170	169	imaeq2d	$⊢ φ \to O [⋃ dom O] = O [dom O ∖ \{⋃ dom O\}]$
171		dff1o3	$⊢ O : dom O \underset{1-1 onto}{⟶} F supp \emptyset \leftrightarrow (O : dom O \underset{onto}{⟶} F supp \emptyset \land Fun O^{-1})$
172	171	simprbi	$⊢ O : dom O \underset{1-1 onto}{⟶} F supp \emptyset \to Fun O^{-1}$
173		imadif	$⊢ Fun O^{-1} \to O [dom O ∖ \{⋃ dom O\}] = O [dom O] ∖ O [\{⋃ dom O\}]$
174	30 172 173	3syl	$⊢ φ \to O [dom O ∖ \{⋃ dom O\}] = O [dom O] ∖ O [\{⋃ dom O\}]$
175	170 174	eqtrd	$⊢ φ \to O [⋃ dom O] = O [dom O] ∖ O [\{⋃ dom O\}]$
176	7 99	ssneldd	$⊢ φ \to \neg X \in {supp}_{\emptyset} (G)$
177		disjsn	$⊢ {supp}_{\emptyset} (G) \cap \{X\} = \emptyset \leftrightarrow \neg X \in {supp}_{\emptyset} (G)$
178	176 177	sylibr	$⊢ φ \to {supp}_{\emptyset} (G) \cap \{X\} = \emptyset$
179		fvex	$⊢ G (X) \in V$
180		dif1o	$⊢ G (X) \in (V ∖ 1_{𝑜}) \leftrightarrow (G (X) \in V \land G (X) \neq \emptyset)$
181	179 180	mpbiran	$⊢ G (X) \in (V ∖ 1_{𝑜}) \leftrightarrow G (X) \neq \emptyset$
182	41	ffnd	$⊢ φ \to G Fn B$
183		elsuppfn	$⊢ (G Fn B \land B \in On \land \emptyset \in V) \to (X \in {supp}_{\emptyset} (G) \leftrightarrow (X \in B \land G (X) \neq \emptyset))$
184	182 3 47 183	syl3anc	$⊢ φ \to (X \in {supp}_{\emptyset} (G) \leftrightarrow (X \in B \land G (X) \neq \emptyset))$
185	181	a1i	$⊢ φ \to (G (X) \in (V ∖ 1_{𝑜}) \leftrightarrow G (X) \neq \emptyset)$
186	185	bicomd	$⊢ φ \to (G (X) \neq \emptyset \leftrightarrow G (X) \in (V ∖ 1_{𝑜}))$
187	186	anbi2d	$⊢ φ \to ((X \in B \land G (X) \neq \emptyset) \leftrightarrow (X \in B \land G (X) \in (V ∖ 1_{𝑜})))$
188	184 187	bitrd	$⊢ φ \to (X \in {supp}_{\emptyset} (G) \leftrightarrow (X \in B \land G (X) \in (V ∖ 1_{𝑜})))$
189	7	sseld	$⊢ φ \to (X \in {supp}_{\emptyset} (G) \to X \in X)$
190	188 189	sylbird	$⊢ φ \to ((X \in B \land G (X) \in (V ∖ 1_{𝑜})) \to X \in X)$
191	5 190	mpand	$⊢ φ \to (G (X) \in (V ∖ 1_{𝑜}) \to X \in X)$
192	181 191	biimtrrid	$⊢ φ \to (G (X) \neq \emptyset \to X \in X)$
193	192	necon1bd	$⊢ φ \to (\neg X \in X \to G (X) = \emptyset)$
194	99 193	mpd	$⊢ φ \to G (X) = \emptyset$
195	194	adantr	$⊢ (φ \land k \in (B ∖ {supp}_{\emptyset} (F))) \to G (X) = \emptyset$
196		fveqeq2	$⊢ k = X \to (G (k) = \emptyset \leftrightarrow G (X) = \emptyset)$
197	195 196	syl5ibrcom	$⊢ (φ \land k \in (B ∖ {supp}_{\emptyset} (F))) \to (k = X \to G (k) = \emptyset)$
198		eldifi	$⊢ k \in (B ∖ {supp}_{\emptyset} (F)) \to k \in B$
199	198	adantl	$⊢ (φ \land k \in (B ∖ {supp}_{\emptyset} (F))) \to k \in B$
200	6	adantr	$⊢ (φ \land k \in (B ∖ {supp}_{\emptyset} (F))) \to Y \in A$
201	200 110 111	sylancl	$⊢ (φ \land k \in (B ∖ {supp}_{\emptyset} (F))) \to if (k = X, Y, G (k)) \in V$
202	8 106 199 201	fvmptd3	$⊢ (φ \land k \in (B ∖ {supp}_{\emptyset} (F))) \to F (k) = if (k = X, Y, G (k))$
203		ssidd	$⊢ φ \to F supp \emptyset \subseteq F supp \emptyset$
204	44 203 3 9	suppssr	$⊢ (φ \land k \in (B ∖ {supp}_{\emptyset} (F))) \to F (k) = \emptyset$
205	202 204	eqtr3d	$⊢ (φ \land k \in (B ∖ {supp}_{\emptyset} (F))) \to if (k = X, Y, G (k)) = \emptyset$
206		iffalse	$⊢ \neg k = X \to if (k = X, Y, G (k)) = G (k)$
207	206	eqeq1d	$⊢ \neg k = X \to (if (k = X, Y, G (k)) = \emptyset \leftrightarrow G (k) = \emptyset)$
208	205 207	syl5ibcom	$⊢ (φ \land k \in (B ∖ {supp}_{\emptyset} (F))) \to (\neg k = X \to G (k) = \emptyset)$
209	197 208	pm2.61d	$⊢ (φ \land k \in (B ∖ {supp}_{\emptyset} (F))) \to G (k) = \emptyset$
210	41 209	suppss	$⊢ φ \to G supp \emptyset \subseteq F supp \emptyset$
211		reldisj	$⊢ G supp \emptyset \subseteq F supp \emptyset \to ({supp}_{\emptyset} (G) \cap \{X\} = \emptyset \leftrightarrow G supp \emptyset \subseteq {supp}_{\emptyset} (F) ∖ \{X\})$
212	210 211	syl	$⊢ φ \to ({supp}_{\emptyset} (G) \cap \{X\} = \emptyset \leftrightarrow G supp \emptyset \subseteq {supp}_{\emptyset} (F) ∖ \{X\})$
213	178 212	mpbid	$⊢ φ \to G supp \emptyset \subseteq {supp}_{\emptyset} (F) ∖ \{X\}$
214		uncom	$⊢ {supp}_{\emptyset} (G) \cup \{X\} = \{X\} \cup {supp}_{\emptyset} (G)$
215	129 214	sseqtrdi	$⊢ φ \to F supp \emptyset \subseteq \{X\} \cup {supp}_{\emptyset} (G)$
216		ssundif	$⊢ F supp \emptyset \subseteq \{X\} \cup {supp}_{\emptyset} (G) \leftrightarrow {supp}_{\emptyset} (F) ∖ \{X\} \subseteq G supp \emptyset$
217	215 216	sylib	$⊢ φ \to {supp}_{\emptyset} (F) ∖ \{X\} \subseteq G supp \emptyset$
218	213 217	eqssd	$⊢ φ \to G supp \emptyset = {supp}_{\emptyset} (F) ∖ \{X\}$
219	157 175 218	3eqtr4rd	$⊢ φ \to G supp \emptyset = O [⋃ dom O]$
220		isores3	$⊢ (O {Isom}_{E, E} (dom O, F supp \emptyset) \land ⋃ dom O \subseteq dom O \land G supp \emptyset = O [⋃ dom O]) \to ({O ↾}_{⋃ dom O}) {Isom}_{E, E} (⋃ dom O, G supp \emptyset)$
221	28 146 219 220	syl3anc	$⊢ φ \to ({O ↾}_{⋃ dom O}) {Isom}_{E, E} (⋃ dom O, G supp \emptyset)$
222	1 2 3 12 4	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (G) \land dom K \in ω)$
223	222	simpld	$⊢ φ \to E We {supp}_{\emptyset} (G)$
224		epse	$⊢ E Se {supp}_{\emptyset} (G)$
225	12	oieu	$⊢ (E We {supp}_{\emptyset} (G) \land E Se {supp}_{\emptyset} (G)) \to ((Ord ⋃ dom O \land ({O ↾}_{⋃ dom O}) {Isom}_{E, E} (⋃ dom O, G supp \emptyset)) \leftrightarrow (⋃ dom O = dom K \land {O ↾}_{⋃ dom O} = K))$
226	223 224 225	sylancl	$⊢ φ \to ((Ord ⋃ dom O \land ({O ↾}_{⋃ dom O}) {Isom}_{E, E} (⋃ dom O, G supp \emptyset)) \leftrightarrow (⋃ dom O = dom K \land {O ↾}_{⋃ dom O} = K))$
227	144 221 226	mpbi2and	$⊢ φ \to (⋃ dom O = dom K \land {O ↾}_{⋃ dom O} = K)$
228	227	simpld	$⊢ φ \to ⋃ dom O = dom K$
229	228	fveq2d	$⊢ φ \to M (⋃ dom O) = M (dom K)$
230		eleq1	$⊢ x = \emptyset \to (x \in dom O \leftrightarrow \emptyset \in dom O)$
231		fveq2	$⊢ x = \emptyset \to H (x) = H (\emptyset)$
232		fveq2	$⊢ x = \emptyset \to M (x) = M (\emptyset)$
233	13	seqom0g	$⊢ \emptyset \in V \to M (\emptyset) = \emptyset$
234	46 233	ax-mp	$⊢ M (\emptyset) = \emptyset$
235	232 234	eqtrdi	$⊢ x = \emptyset \to M (x) = \emptyset$
236	231 235	eqeq12d	$⊢ x = \emptyset \to (H (x) = M (x) \leftrightarrow H (\emptyset) = \emptyset)$
237	230 236	imbi12d	$⊢ x = \emptyset \to ((x \in dom O \to H (x) = M (x)) \leftrightarrow (\emptyset \in dom O \to H (\emptyset) = \emptyset))$
238	237	imbi2d	$⊢ x = \emptyset \to ((φ \to (x \in dom O \to H (x) = M (x))) \leftrightarrow (φ \to (\emptyset \in dom O \to H (\emptyset) = \emptyset)))$
239		eleq1	$⊢ x = y \to (x \in dom O \leftrightarrow y \in dom O)$
240		fveq2	$⊢ x = y \to H (x) = H (y)$
241		fveq2	$⊢ x = y \to M (x) = M (y)$
242	240 241	eqeq12d	$⊢ x = y \to (H (x) = M (x) \leftrightarrow H (y) = M (y))$
243	239 242	imbi12d	$⊢ x = y \to ((x \in dom O \to H (x) = M (x)) \leftrightarrow (y \in dom O \to H (y) = M (y)))$
244	243	imbi2d	$⊢ x = y \to ((φ \to (x \in dom O \to H (x) = M (x))) \leftrightarrow (φ \to (y \in dom O \to H (y) = M (y))))$
245		eleq1	$⊢ x = suc y \to (x \in dom O \leftrightarrow suc y \in dom O)$
246		fveq2	$⊢ x = suc y \to H (x) = H (suc y)$
247		fveq2	$⊢ x = suc y \to M (x) = M (suc y)$
248	246 247	eqeq12d	$⊢ x = suc y \to (H (x) = M (x) \leftrightarrow H (suc y) = M (suc y))$
249	245 248	imbi12d	$⊢ x = suc y \to ((x \in dom O \to H (x) = M (x)) \leftrightarrow (suc y \in dom O \to H (suc y) = M (suc y)))$
250	249	imbi2d	$⊢ x = suc y \to ((φ \to (x \in dom O \to H (x) = M (x))) \leftrightarrow (φ \to (suc y \in dom O \to H (suc y) = M (suc y))))$
251		eleq1	$⊢ x = ⋃ dom O \to (x \in dom O \leftrightarrow ⋃ dom O \in dom O)$
252		fveq2	$⊢ x = ⋃ dom O \to H (x) = H (⋃ dom O)$
253		fveq2	$⊢ x = ⋃ dom O \to M (x) = M (⋃ dom O)$
254	252 253	eqeq12d	$⊢ x = ⋃ dom O \to (H (x) = M (x) \leftrightarrow H (⋃ dom O) = M (⋃ dom O))$
255	251 254	imbi12d	$⊢ x = ⋃ dom O \to ((x \in dom O \to H (x) = M (x)) \leftrightarrow (⋃ dom O \in dom O \to H (⋃ dom O) = M (⋃ dom O)))$
256	255	imbi2d	$⊢ x = ⋃ dom O \to ((φ \to (x \in dom O \to H (x) = M (x))) \leftrightarrow (φ \to (⋃ dom O \in dom O \to H (⋃ dom O) = M (⋃ dom O))))$
257	11	seqom0g	$⊢ \emptyset \in dom O \to H (\emptyset) = \emptyset$
258	257	a1i	$⊢ φ \to (\emptyset \in dom O \to H (\emptyset) = \emptyset)$
259		nnord	$⊢ dom O \in ω \to Ord dom O$
260	19 259	syl	$⊢ φ \to Ord dom O$
261		ordtr	$⊢ Ord dom O \to Tr dom O$
262	260 261	syl	$⊢ φ \to Tr dom O$
263		trsuc	$⊢ (Tr dom O \land suc y \in dom O) \to y \in dom O$
264	262 263	sylan	$⊢ (φ \land suc y \in dom O) \to y \in dom O$
265	264	ex	$⊢ φ \to (suc y \in dom O \to y \in dom O)$
266	265	imim1d	$⊢ φ \to ((y \in dom O \to H (y) = M (y)) \to (suc y \in dom O \to H (y) = M (y)))$
267		oveq2	$⊢ H (y) = M (y) \to ((A ↑_{𝑜} O (y)) \cdot_{𝑜} F (O (y))) +_{𝑜} H (y) = ((A ↑_{𝑜} O (y)) \cdot_{𝑜} F (O (y))) +_{𝑜} M (y)$
268		elnn	$⊢ (y \in dom O \land dom O \in ω) \to y \in ω$
269	268	ancoms	$⊢ (dom O \in ω \land y \in dom O) \to y \in ω$
270	19 264 269	syl2an2r	$⊢ (φ \land suc y \in dom O) \to y \in ω$
271	1 2 3 10 14 11	cantnfsuc	$⊢ (φ \land y \in ω) \to H (suc y) = ((A ↑_{𝑜} O (y)) \cdot_{𝑜} F (O (y))) +_{𝑜} H (y)$
272	270 271	syldan	$⊢ (φ \land suc y \in dom O) \to H (suc y) = ((A ↑_{𝑜} O (y)) \cdot_{𝑜} F (O (y))) +_{𝑜} H (y)$
273	1 2 3 12 4 13	cantnfsuc	$⊢ (φ \land y \in ω) \to M (suc y) = ((A ↑_{𝑜} K (y)) \cdot_{𝑜} G (K (y))) +_{𝑜} M (y)$
274	270 273	syldan	$⊢ (φ \land suc y \in dom O) \to M (suc y) = ((A ↑_{𝑜} K (y)) \cdot_{𝑜} G (K (y))) +_{𝑜} M (y)$
275	227	simprd	$⊢ φ \to {O ↾}_{⋃ dom O} = K$
276	275	fveq1d	$⊢ φ \to ({O ↾}_{⋃ dom O}) (y) = K (y)$
277	276	adantr	$⊢ (φ \land suc y \in dom O) \to ({O ↾}_{⋃ dom O}) (y) = K (y)$
278	16	eleq2d	$⊢ φ \to (suc y \in dom O \leftrightarrow suc y \in suc ⋃ dom O)$
279	278	biimpa	$⊢ (φ \land suc y \in dom O) \to suc y \in suc ⋃ dom O$
280	144	adantr	$⊢ (φ \land suc y \in dom O) \to Ord ⋃ dom O$
281		ordsucelsuc	$⊢ Ord ⋃ dom O \to (y \in ⋃ dom O \leftrightarrow suc y \in suc ⋃ dom O)$
282	280 281	syl	$⊢ (φ \land suc y \in dom O) \to (y \in ⋃ dom O \leftrightarrow suc y \in suc ⋃ dom O)$
283	279 282	mpbird	$⊢ (φ \land suc y \in dom O) \to y \in ⋃ dom O$
284	283	fvresd	$⊢ (φ \land suc y \in dom O) \to ({O ↾}_{⋃ dom O}) (y) = O (y)$
285	277 284	eqtr3d	$⊢ (φ \land suc y \in dom O) \to K (y) = O (y)$
286	285	oveq2d	$⊢ (φ \land suc y \in dom O) \to A ↑_{𝑜} K (y) = A ↑_{𝑜} O (y)$
287		eqeq1	$⊢ t = K (y) \to (t = X \leftrightarrow K (y) = X)$
288		fveq2	$⊢ t = K (y) \to G (t) = G (K (y))$
289	287 288	ifbieq2d	$⊢ t = K (y) \to if (t = X, Y, G (t)) = if (K (y) = X, Y, G (K (y)))$
290		suppssdm	$⊢ G supp \emptyset \subseteq dom G$
291	290 41	fssdm	$⊢ φ \to G supp \emptyset \subseteq B$
292	291	adantr	$⊢ (φ \land suc y \in dom O) \to G supp \emptyset \subseteq B$
293	228	adantr	$⊢ (φ \land suc y \in dom O) \to ⋃ dom O = dom K$
294	283 293	eleqtrd	$⊢ (φ \land suc y \in dom O) \to y \in dom K$
295	12	oif	$⊢ K : dom K ⟶ G supp \emptyset$
296	295	ffvelcdmi	$⊢ y \in dom K \to K (y) \in {supp}_{\emptyset} (G)$
297	294 296	syl	$⊢ (φ \land suc y \in dom O) \to K (y) \in {supp}_{\emptyset} (G)$
298	292 297	sseldd	$⊢ (φ \land suc y \in dom O) \to K (y) \in B$
299	6	adantr	$⊢ (φ \land suc y \in dom O) \to Y \in A$
300		fvex	$⊢ G (K (y)) \in V$
301		ifexg	$⊢ (Y \in A \land G (K (y)) \in V) \to if (K (y) = X, Y, G (K (y))) \in V$
302	299 300 301	sylancl	$⊢ (φ \land suc y \in dom O) \to if (K (y) = X, Y, G (K (y))) \in V$
303	8 289 298 302	fvmptd3	$⊢ (φ \land suc y \in dom O) \to F (K (y)) = if (K (y) = X, Y, G (K (y)))$
304	285	fveq2d	$⊢ (φ \land suc y \in dom O) \to F (K (y)) = F (O (y))$
305	176	adantr	$⊢ (φ \land suc y \in dom O) \to \neg X \in {supp}_{\emptyset} (G)$
306		nelneq	$⊢ (K (y) \in {supp}_{\emptyset} (G) \land \neg X \in {supp}_{\emptyset} (G)) \to \neg K (y) = X$
307	297 305 306	syl2anc	$⊢ (φ \land suc y \in dom O) \to \neg K (y) = X$
308	307	iffalsed	$⊢ (φ \land suc y \in dom O) \to if (K (y) = X, Y, G (K (y))) = G (K (y))$
309	303 304 308	3eqtr3rd	$⊢ (φ \land suc y \in dom O) \to G (K (y)) = F (O (y))$
310	286 309	oveq12d	$⊢ (φ \land suc y \in dom O) \to (A ↑_{𝑜} K (y)) \cdot_{𝑜} G (K (y)) = (A ↑_{𝑜} O (y)) \cdot_{𝑜} F (O (y))$
311	310	oveq1d	$⊢ (φ \land suc y \in dom O) \to ((A ↑_{𝑜} K (y)) \cdot_{𝑜} G (K (y))) +_{𝑜} M (y) = ((A ↑_{𝑜} O (y)) \cdot_{𝑜} F (O (y))) +_{𝑜} M (y)$
312	274 311	eqtrd	$⊢ (φ \land suc y \in dom O) \to M (suc y) = ((A ↑_{𝑜} O (y)) \cdot_{𝑜} F (O (y))) +_{𝑜} M (y)$
313	272 312	eqeq12d	$⊢ (φ \land suc y \in dom O) \to (H (suc y) = M (suc y) \leftrightarrow ((A ↑_{𝑜} O (y)) \cdot_{𝑜} F (O (y))) +_{𝑜} H (y) = ((A ↑_{𝑜} O (y)) \cdot_{𝑜} F (O (y))) +_{𝑜} M (y))$
314	267 313	imbitrrid	$⊢ (φ \land suc y \in dom O) \to (H (y) = M (y) \to H (suc y) = M (suc y))$
315	314	ex	$⊢ φ \to (suc y \in dom O \to (H (y) = M (y) \to H (suc y) = M (suc y)))$
316	315	a2d	$⊢ φ \to ((suc y \in dom O \to H (y) = M (y)) \to (suc y \in dom O \to H (suc y) = M (suc y)))$
317	266 316	syld	$⊢ φ \to ((y \in dom O \to H (y) = M (y)) \to (suc y \in dom O \to H (suc y) = M (suc y)))$
318	317	a2i	$⊢ (φ \to (y \in dom O \to H (y) = M (y))) \to (φ \to (suc y \in dom O \to H (suc y) = M (suc y)))$
319	318	a1i	$⊢ y \in ω \to ((φ \to (y \in dom O \to H (y) = M (y))) \to (φ \to (suc y \in dom O \to H (suc y) = M (suc y))))$
320	238 244 250 256 258 319	finds	$⊢ ⋃ dom O \in ω \to (φ \to (⋃ dom O \in dom O \to H (⋃ dom O) = M (⋃ dom O)))$
321	22 320	mpcom	$⊢ φ \to (⋃ dom O \in dom O \to H (⋃ dom O) = M (⋃ dom O))$
322	64 321	mpd	$⊢ φ \to H (⋃ dom O) = M (⋃ dom O)$
323	1 2 3 12 4 13	cantnfval	$⊢ φ \to (A CNF B) (G) = M (dom K)$
324	229 322 323	3eqtr4d	$⊢ φ \to H (⋃ dom O) = (A CNF B) (G)$
325	142 324	oveq12d	$⊢ φ \to ((A ↑_{𝑜} O (⋃ dom O)) \cdot_{𝑜} F (O (⋃ dom O))) +_{𝑜} H (⋃ dom O) = ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} (A CNF B) (G)$
326	24 325	eqtrd	$⊢ φ \to H (suc ⋃ dom O) = ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} (A CNF B) (G)$
327	15 17 326	3eqtrd	$⊢ φ \to (A CNF B) (F) = ((A ↑_{𝑜} X) \cdot_{𝑜} Y) +_{𝑜} (A CNF B) (G)$

Metamath Proof Explorer

Theorem cantnfp1lem3

Proof