cantnfle

Description: A lower bound on the CNF function. Since ( ( A CNF B )F ) is defined as the sum of ( A ^o x ) .o ( Fx ) over all x in the support of F , it is larger than any of these terms (and all other terms are zero, so we can extend the statement to all C e. B instead of just those C in the support). (Contributed by Mario Carneiro, 28-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)$
	cantnfle.c	$⊢ φ \to C \in B$
Assertion	cantnfle	$⊢ φ \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq (A CNF B) (F)$

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		cantnfle.c	$⊢ φ \to C \in B$
8		oveq2	$⊢ F (C) = \emptyset \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) = (A ↑_{𝑜} C) \cdot_{𝑜} \emptyset$
9	8	sseq1d	$⊢ F (C) = \emptyset \to ((A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq (A CNF B) (F) \leftrightarrow (A ↑_{𝑜} C) \cdot_{𝑜} \emptyset \subseteq (A CNF B) (F))$
10		ovexd	$⊢ φ \to F supp \emptyset \in V$
11	1 2 3 4 5	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (F) \land dom G \in ω)$
12	11	simpld	$⊢ φ \to E We {supp}_{\emptyset} (F)$
13	4	oiiso	$⊢ (F supp \emptyset \in V \land E We {supp}_{\emptyset} (F)) \to G {Isom}_{E, E} (dom G, F supp \emptyset)$
14	10 12 13	syl2anc	$⊢ φ \to G {Isom}_{E, E} (dom G, F supp \emptyset)$
15		isof1o	$⊢ G {Isom}_{E, E} (dom G, F supp \emptyset) \to G : dom G \underset{1-1 onto}{⟶} F supp \emptyset$
16	14 15	syl	$⊢ φ \to G : dom G \underset{1-1 onto}{⟶} F supp \emptyset$
17	16	adantr	$⊢ (φ \land F (C) \neq \emptyset) \to G : dom G \underset{1-1 onto}{⟶} F supp \emptyset$
18		f1ocnv	$⊢ G : dom G \underset{1-1 onto}{⟶} F supp \emptyset \to G^{-1} : F supp \emptyset \underset{1-1 onto}{⟶} dom G$
19		f1of	$⊢ G^{-1} : F supp \emptyset \underset{1-1 onto}{⟶} dom G \to G^{-1} : F supp \emptyset ⟶ dom G$
20	17 18 19	3syl	$⊢ (φ \land F (C) \neq \emptyset) \to G^{-1} : F supp \emptyset ⟶ dom G$
21	7	anim1i	$⊢ (φ \land F (C) \neq \emptyset) \to (C \in B \land F (C) \neq \emptyset)$
22	1 2 3	cantnfs	$⊢ φ \to (F \in S \leftrightarrow (F : B ⟶ A \land {finSupp}_{\emptyset} (F)))$
23	5 22	mpbid	$⊢ φ \to (F : B ⟶ A \land {finSupp}_{\emptyset} (F))$
24	23	simpld	$⊢ φ \to F : B ⟶ A$
25	24	adantr	$⊢ (φ \land F (C) \neq \emptyset) \to F : B ⟶ A$
26	25	ffnd	$⊢ (φ \land F (C) \neq \emptyset) \to F Fn B$
27	3	adantr	$⊢ (φ \land F (C) \neq \emptyset) \to B \in On$
28		0ex	$⊢ \emptyset \in V$
29	28	a1i	$⊢ (φ \land F (C) \neq \emptyset) \to \emptyset \in V$
30		elsuppfn	$⊢ (F Fn B \land B \in On \land \emptyset \in V) \to (C \in {supp}_{\emptyset} (F) \leftrightarrow (C \in B \land F (C) \neq \emptyset))$
31	26 27 29 30	syl3anc	$⊢ (φ \land F (C) \neq \emptyset) \to (C \in {supp}_{\emptyset} (F) \leftrightarrow (C \in B \land F (C) \neq \emptyset))$
32	21 31	mpbird	$⊢ (φ \land F (C) \neq \emptyset) \to C \in {supp}_{\emptyset} (F)$
33	20 32	ffvelcdmd	$⊢ (φ \land F (C) \neq \emptyset) \to G^{-1} (C) \in dom G$
34	11	simprd	$⊢ φ \to dom G \in ω$
35	34	adantr	$⊢ (φ \land F (C) \neq \emptyset) \to dom G \in ω$
36		eqimss	$⊢ x = dom G \to x \subseteq dom G$
37	36	biantrurd	$⊢ x = dom G \to (G^{-1} (C) \in x \leftrightarrow (x \subseteq dom G \land G^{-1} (C) \in x))$
38		eleq2	$⊢ x = dom G \to (G^{-1} (C) \in x \leftrightarrow G^{-1} (C) \in dom G)$
39	37 38	bitr3d	$⊢ x = dom G \to ((x \subseteq dom G \land G^{-1} (C) \in x) \leftrightarrow G^{-1} (C) \in dom G)$
40		fveq2	$⊢ x = dom G \to H (x) = H (dom G)$
41	40	sseq2d	$⊢ x = dom G \to ((A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (x) \leftrightarrow (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (dom G))$
42	39 41	imbi12d	$⊢ x = dom G \to (((x \subseteq dom G \land G^{-1} (C) \in x) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (x)) \leftrightarrow (G^{-1} (C) \in dom G \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (dom G)))$
43	42	imbi2d	$⊢ x = dom G \to (((φ \land F (C) \neq \emptyset) \to ((x \subseteq dom G \land G^{-1} (C) \in x) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (x))) \leftrightarrow ((φ \land F (C) \neq \emptyset) \to (G^{-1} (C) \in dom G \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (dom G))))$
44		sseq1	$⊢ x = \emptyset \to (x \subseteq dom G \leftrightarrow \emptyset \subseteq dom G)$
45		eleq2	$⊢ x = \emptyset \to (G^{-1} (C) \in x \leftrightarrow G^{-1} (C) \in \emptyset)$
46	44 45	anbi12d	$⊢ x = \emptyset \to ((x \subseteq dom G \land G^{-1} (C) \in x) \leftrightarrow (\emptyset \subseteq dom G \land G^{-1} (C) \in \emptyset))$
47		fveq2	$⊢ x = \emptyset \to H (x) = H (\emptyset)$
48	47	sseq2d	$⊢ x = \emptyset \to ((A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (x) \leftrightarrow (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (\emptyset))$
49	46 48	imbi12d	$⊢ x = \emptyset \to (((x \subseteq dom G \land G^{-1} (C) \in x) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (x)) \leftrightarrow ((\emptyset \subseteq dom G \land G^{-1} (C) \in \emptyset) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (\emptyset)))$
50		sseq1	$⊢ x = y \to (x \subseteq dom G \leftrightarrow y \subseteq dom G)$
51		eleq2	$⊢ x = y \to (G^{-1} (C) \in x \leftrightarrow G^{-1} (C) \in y)$
52	50 51	anbi12d	$⊢ x = y \to ((x \subseteq dom G \land G^{-1} (C) \in x) \leftrightarrow (y \subseteq dom G \land G^{-1} (C) \in y))$
53		fveq2	$⊢ x = y \to H (x) = H (y)$
54	53	sseq2d	$⊢ x = y \to ((A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (x) \leftrightarrow (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y))$
55	52 54	imbi12d	$⊢ x = y \to (((x \subseteq dom G \land G^{-1} (C) \in x) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (x)) \leftrightarrow ((y \subseteq dom G \land G^{-1} (C) \in y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y)))$
56		sseq1	$⊢ x = suc y \to (x \subseteq dom G \leftrightarrow suc y \subseteq dom G)$
57		eleq2	$⊢ x = suc y \to (G^{-1} (C) \in x \leftrightarrow G^{-1} (C) \in suc y)$
58	56 57	anbi12d	$⊢ x = suc y \to ((x \subseteq dom G \land G^{-1} (C) \in x) \leftrightarrow (suc y \subseteq dom G \land G^{-1} (C) \in suc y))$
59		fveq2	$⊢ x = suc y \to H (x) = H (suc y)$
60	59	sseq2d	$⊢ x = suc y \to ((A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (x) \leftrightarrow (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y))$
61	58 60	imbi12d	$⊢ x = suc y \to (((x \subseteq dom G \land G^{-1} (C) \in x) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (x)) \leftrightarrow ((suc y \subseteq dom G \land G^{-1} (C) \in suc y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y)))$
62		noel	$⊢ \neg G^{-1} (C) \in \emptyset$
63	62	pm2.21i	$⊢ G^{-1} (C) \in \emptyset \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (\emptyset)$
64	63	adantl	$⊢ (\emptyset \subseteq dom G \land G^{-1} (C) \in \emptyset) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (\emptyset)$
65	64	a1i	$⊢ (φ \land F (C) \neq \emptyset) \to ((\emptyset \subseteq dom G \land G^{-1} (C) \in \emptyset) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (\emptyset))$
66		fvex	$⊢ G^{-1} (C) \in V$
67	66	elsuc	$⊢ G^{-1} (C) \in suc y \leftrightarrow (G^{-1} (C) \in y \lor G^{-1} (C) = y)$
68		sssucid	$⊢ y \subseteq suc y$
69		sstr	$⊢ (y \subseteq suc y \land suc y \subseteq dom G) \to y \subseteq dom G$
70	68 69	mpan	$⊢ suc y \subseteq dom G \to y \subseteq dom G$
71	70	ad2antrl	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) \in y)) \to y \subseteq dom G$
72		simprr	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) \in y)) \to G^{-1} (C) \in y$
73		pm2.27	$⊢ (y \subseteq dom G \land G^{-1} (C) \in y) \to (((y \subseteq dom G \land G^{-1} (C) \in y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y)) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y))$
74	71 72 73	syl2anc	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) \in y)) \to (((y \subseteq dom G \land G^{-1} (C) \in y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y)) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y))$
75	6	cantnfvalf	$⊢ H : ω ⟶ On$
76	75	ffvelcdmi	$⊢ y \in ω \to H (y) \in On$
77	76	ad2antlr	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to H (y) \in On$
78	2	ad3antrrr	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to A \in On$
79	3	ad3antrrr	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to B \in On$
80		suppssdm	$⊢ F supp \emptyset \subseteq dom F$
81	80 24	fssdm	$⊢ φ \to F supp \emptyset \subseteq B$
82	81	ad3antrrr	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to F supp \emptyset \subseteq B$
83		simpr	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to suc y \subseteq dom G$
84		sucidg	$⊢ y \in ω \to y \in suc y$
85	84	ad2antlr	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to y \in suc y$
86	83 85	sseldd	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to y \in dom G$
87	4	oif	$⊢ G : dom G ⟶ F supp \emptyset$
88	87	ffvelcdmi	$⊢ y \in dom G \to G (y) \in {supp}_{\emptyset} (F)$
89	86 88	syl	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to G (y) \in {supp}_{\emptyset} (F)$
90	82 89	sseldd	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to G (y) \in B$
91		onelon	$⊢ (B \in On \land G (y) \in B) \to G (y) \in On$
92	79 90 91	syl2anc	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to G (y) \in On$
93		oecl	$⊢ (A \in On \land G (y) \in On) \to A ↑_{𝑜} G (y) \in On$
94	78 92 93	syl2anc	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to A ↑_{𝑜} G (y) \in On$
95	24	ad3antrrr	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to F : B ⟶ A$
96	95 90	ffvelcdmd	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to F (G (y)) \in A$
97		onelon	$⊢ (A \in On \land F (G (y)) \in A) \to F (G (y)) \in On$
98	78 96 97	syl2anc	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to F (G (y)) \in On$
99		omcl	$⊢ (A ↑_{𝑜} G (y) \in On \land F (G (y)) \in On) \to (A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)) \in On$
100	94 98 99	syl2anc	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to (A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)) \in On$
101		oaword2	$⊢ (H (y) \in On \land (A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)) \in On) \to H (y) \subseteq ((A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))) +_{𝑜} H (y)$
102	77 100 101	syl2anc	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to H (y) \subseteq ((A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))) +_{𝑜} H (y)$
103	1 2 3 4 5 6	cantnfsuc	$⊢ (φ \land y \in ω) \to H (suc y) = ((A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))) +_{𝑜} H (y)$
104	103	ad4ant13	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to H (suc y) = ((A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))) +_{𝑜} H (y)$
105	102 104	sseqtrrd	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to H (y) \subseteq H (suc y)$
106		sstr	$⊢ ((A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y) \land H (y) \subseteq H (suc y)) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y)$
107	106	expcom	$⊢ H (y) \subseteq H (suc y) \to ((A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y))$
108	105 107	syl	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to ((A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y))$
109	108	adantrr	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) \in y)) \to ((A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y))$
110	74 109	syld	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) \in y)) \to (((y \subseteq dom G \land G^{-1} (C) \in y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y)) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y))$
111	110	expr	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to (G^{-1} (C) \in y \to (((y \subseteq dom G \land G^{-1} (C) \in y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y)) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y)))$
112		simprr	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) = y)) \to G^{-1} (C) = y$
113	112	fveq2d	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) = y)) \to G (G^{-1} (C)) = G (y)$
114		f1ocnvfv2	$⊢ (G : dom G \underset{1-1 onto}{⟶} F supp \emptyset \land C \in {supp}_{\emptyset} (F)) \to G (G^{-1} (C)) = C$
115	17 32 114	syl2anc	$⊢ (φ \land F (C) \neq \emptyset) \to G (G^{-1} (C)) = C$
116	115	ad2antrr	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) = y)) \to G (G^{-1} (C)) = C$
117	113 116	eqtr3d	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) = y)) \to G (y) = C$
118	117	oveq2d	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) = y)) \to A ↑_{𝑜} G (y) = A ↑_{𝑜} C$
119	117	fveq2d	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) = y)) \to F (G (y)) = F (C)$
120	118 119	oveq12d	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) = y)) \to (A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)) = (A ↑_{𝑜} C) \cdot_{𝑜} F (C)$
121		oaword1	$⊢ ((A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)) \in On \land H (y) \in On) \to (A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)) \subseteq ((A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))) +_{𝑜} H (y)$
122	100 77 121	syl2anc	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to (A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)) \subseteq ((A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))) +_{𝑜} H (y)$
123	122	adantrr	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) = y)) \to (A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y)) \subseteq ((A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))) +_{𝑜} H (y)$
124	120 123	eqsstrrd	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) = y)) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq ((A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))) +_{𝑜} H (y)$
125	103	ad4ant13	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) = y)) \to H (suc y) = ((A ↑_{𝑜} G (y)) \cdot_{𝑜} F (G (y))) +_{𝑜} H (y)$
126	124 125	sseqtrrd	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land (suc y \subseteq dom G \land G^{-1} (C) = y)) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y)$
127	126	expr	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to (G^{-1} (C) = y \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y))$
128	127	a1dd	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to (G^{-1} (C) = y \to (((y \subseteq dom G \land G^{-1} (C) \in y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y)) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y)))$
129	111 128	jaod	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to ((G^{-1} (C) \in y \lor G^{-1} (C) = y) \to (((y \subseteq dom G \land G^{-1} (C) \in y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y)) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y)))$
130	67 129	biimtrid	$⊢ (((φ \land F (C) \neq \emptyset) \land y \in ω) \land suc y \subseteq dom G) \to (G^{-1} (C) \in suc y \to (((y \subseteq dom G \land G^{-1} (C) \in y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y)) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y)))$
131	130	expimpd	$⊢ ((φ \land F (C) \neq \emptyset) \land y \in ω) \to ((suc y \subseteq dom G \land G^{-1} (C) \in suc y) \to (((y \subseteq dom G \land G^{-1} (C) \in y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y)) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y)))$
132	131	com23	$⊢ ((φ \land F (C) \neq \emptyset) \land y \in ω) \to (((y \subseteq dom G \land G^{-1} (C) \in y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y)) \to ((suc y \subseteq dom G \land G^{-1} (C) \in suc y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y)))$
133	132	expcom	$⊢ y \in ω \to ((φ \land F (C) \neq \emptyset) \to (((y \subseteq dom G \land G^{-1} (C) \in y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (y)) \to ((suc y \subseteq dom G \land G^{-1} (C) \in suc y) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (suc y))))$
134	49 55 61 65 133	finds2	$⊢ x \in ω \to ((φ \land F (C) \neq \emptyset) \to ((x \subseteq dom G \land G^{-1} (C) \in x) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (x)))$
135	43 134	vtoclga	$⊢ dom G \in ω \to ((φ \land F (C) \neq \emptyset) \to (G^{-1} (C) \in dom G \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (dom G)))$
136	35 135	mpcom	$⊢ (φ \land F (C) \neq \emptyset) \to (G^{-1} (C) \in dom G \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (dom G))$
137	33 136	mpd	$⊢ (φ \land F (C) \neq \emptyset) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq H (dom G)$
138	1 2 3 4 5 6	cantnfval	$⊢ φ \to (A CNF B) (F) = H (dom G)$
139	138	adantr	$⊢ (φ \land F (C) \neq \emptyset) \to (A CNF B) (F) = H (dom G)$
140	137 139	sseqtrrd	$⊢ (φ \land F (C) \neq \emptyset) \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq (A CNF B) (F)$
141		onelon	$⊢ (B \in On \land C \in B) \to C \in On$
142	3 7 141	syl2anc	$⊢ φ \to C \in On$
143		oecl	$⊢ (A \in On \land C \in On) \to A ↑_{𝑜} C \in On$
144	2 142 143	syl2anc	$⊢ φ \to A ↑_{𝑜} C \in On$
145		om0	$⊢ A ↑_{𝑜} C \in On \to (A ↑_{𝑜} C) \cdot_{𝑜} \emptyset = \emptyset$
146	144 145	syl	$⊢ φ \to (A ↑_{𝑜} C) \cdot_{𝑜} \emptyset = \emptyset$
147		0ss	$⊢ \emptyset \subseteq (A CNF B) (F)$
148	146 147	eqsstrdi	$⊢ φ \to (A ↑_{𝑜} C) \cdot_{𝑜} \emptyset \subseteq (A CNF B) (F)$
149	9 140 148	pm2.61ne	$⊢ φ \to (A ↑_{𝑜} C) \cdot_{𝑜} F (C) \subseteq (A CNF B) (F)$

Metamath Proof Explorer

Theorem cantnfle

Proof