cantnflem1d

Description: Lemma for cantnf . (Contributed by Mario Carneiro, 4-Jun-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	cantnflem1d	$⊢ φ \to (A CNF B) ((x \in B ⟼ if (x \subseteq X, F (x), \emptyset))) \in H (suc O^{-1} (X))$

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	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)))$
12	11	simp1d	$⊢ φ \to X \in B$
13		onelon	$⊢ (B \in On \land X \in B) \to X \in On$
14	3 12 13	syl2anc	$⊢ φ \to X \in On$
15		oecl	$⊢ (A \in On \land X \in On) \to A ↑_{𝑜} X \in On$
16	2 14 15	syl2anc	$⊢ φ \to A ↑_{𝑜} X \in On$
17	1 2 3	cantnfs	$⊢ φ \to (G \in S \leftrightarrow (G : B ⟶ A \land {finSupp}_{\emptyset} (G)))$
18	6 17	mpbid	$⊢ φ \to (G : B ⟶ A \land {finSupp}_{\emptyset} (G))$
19	18	simpld	$⊢ φ \to G : B ⟶ A$
20	19 12	ffvelcdmd	$⊢ φ \to G (X) \in A$
21		onelon	$⊢ (A \in On \land G (X) \in A) \to G (X) \in On$
22	2 20 21	syl2anc	$⊢ φ \to G (X) \in On$
23		omcl	$⊢ (A ↑_{𝑜} X \in On \land G (X) \in On) \to (A ↑_{𝑜} X) \cdot_{𝑜} G (X) \in On$
24	16 22 23	syl2anc	$⊢ φ \to (A ↑_{𝑜} X) \cdot_{𝑜} G (X) \in On$
25		ovexd	$⊢ φ \to G supp \emptyset \in V$
26	1 2 3 9 6	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (G) \land dom O \in ω)$
27	26	simpld	$⊢ φ \to E We {supp}_{\emptyset} (G)$
28	9	oiiso	$⊢ (G supp \emptyset \in V \land E We {supp}_{\emptyset} (G)) \to O {Isom}_{E, E} (dom O, G supp \emptyset)$
29	25 27 28	syl2anc	$⊢ φ \to O {Isom}_{E, E} (dom O, G supp \emptyset)$
30		isof1o	$⊢ O {Isom}_{E, E} (dom O, G supp \emptyset) \to O : dom O \underset{1-1 onto}{⟶} G supp \emptyset$
31	29 30	syl	$⊢ φ \to O : dom O \underset{1-1 onto}{⟶} G supp \emptyset$
32		f1ocnv	$⊢ O : dom O \underset{1-1 onto}{⟶} G supp \emptyset \to O^{-1} : G supp \emptyset \underset{1-1 onto}{⟶} dom O$
33		f1of	$⊢ O^{-1} : G supp \emptyset \underset{1-1 onto}{⟶} dom O \to O^{-1} : G supp \emptyset ⟶ dom O$
34	31 32 33	3syl	$⊢ φ \to O^{-1} : G supp \emptyset ⟶ dom O$
35	1 2 3 4 5 6 7 8	cantnflem1a	$⊢ φ \to X \in {supp}_{\emptyset} (G)$
36	34 35	ffvelcdmd	$⊢ φ \to O^{-1} (X) \in dom O$
37	26	simprd	$⊢ φ \to dom O \in ω$
38		elnn	$⊢ (O^{-1} (X) \in dom O \land dom O \in ω) \to O^{-1} (X) \in ω$
39	36 37 38	syl2anc	$⊢ φ \to O^{-1} (X) \in ω$
40	10	cantnfvalf	$⊢ H : ω ⟶ On$
41	40	ffvelcdmi	$⊢ O^{-1} (X) \in ω \to H (O^{-1} (X)) \in On$
42	39 41	syl	$⊢ φ \to H (O^{-1} (X)) \in On$
43		oaword1	$⊢ ((A ↑_{𝑜} X) \cdot_{𝑜} G (X) \in On \land H (O^{-1} (X)) \in On) \to (A ↑_{𝑜} X) \cdot_{𝑜} G (X) \subseteq ((A ↑_{𝑜} X) \cdot_{𝑜} G (X)) +_{𝑜} H (O^{-1} (X))$
44	24 42 43	syl2anc	$⊢ φ \to (A ↑_{𝑜} X) \cdot_{𝑜} G (X) \subseteq ((A ↑_{𝑜} X) \cdot_{𝑜} G (X)) +_{𝑜} H (O^{-1} (X))$
45	1 2 3 9 6 10	cantnfsuc	$⊢ (φ \land O^{-1} (X) \in ω) \to H (suc O^{-1} (X)) = ((A ↑_{𝑜} O (O^{-1} (X))) \cdot_{𝑜} G (O (O^{-1} (X)))) +_{𝑜} H (O^{-1} (X))$
46	39 45	mpdan	$⊢ φ \to H (suc O^{-1} (X)) = ((A ↑_{𝑜} O (O^{-1} (X))) \cdot_{𝑜} G (O (O^{-1} (X)))) +_{𝑜} H (O^{-1} (X))$
47		f1ocnvfv2	$⊢ (O : dom O \underset{1-1 onto}{⟶} G supp \emptyset \land X \in {supp}_{\emptyset} (G)) \to O (O^{-1} (X)) = X$
48	31 35 47	syl2anc	$⊢ φ \to O (O^{-1} (X)) = X$
49	48	oveq2d	$⊢ φ \to A ↑_{𝑜} O (O^{-1} (X)) = A ↑_{𝑜} X$
50	48	fveq2d	$⊢ φ \to G (O (O^{-1} (X))) = G (X)$
51	49 50	oveq12d	$⊢ φ \to (A ↑_{𝑜} O (O^{-1} (X))) \cdot_{𝑜} G (O (O^{-1} (X))) = (A ↑_{𝑜} X) \cdot_{𝑜} G (X)$
52	51	oveq1d	$⊢ φ \to ((A ↑_{𝑜} O (O^{-1} (X))) \cdot_{𝑜} G (O (O^{-1} (X)))) +_{𝑜} H (O^{-1} (X)) = ((A ↑_{𝑜} X) \cdot_{𝑜} G (X)) +_{𝑜} H (O^{-1} (X))$
53	46 52	eqtrd	$⊢ φ \to H (suc O^{-1} (X)) = ((A ↑_{𝑜} X) \cdot_{𝑜} G (X)) +_{𝑜} H (O^{-1} (X))$
54	44 53	sseqtrrd	$⊢ φ \to (A ↑_{𝑜} X) \cdot_{𝑜} G (X) \subseteq H (suc O^{-1} (X))$
55		onss	$⊢ B \in On \to B \subseteq On$
56	3 55	syl	$⊢ φ \to B \subseteq On$
57	56	sselda	$⊢ (φ \land x \in B) \to x \in On$
58	14	adantr	$⊢ (φ \land x \in B) \to X \in On$
59		onsseleq	$⊢ (x \in On \land X \in On) \to (x \subseteq X \leftrightarrow (x \in X \lor x = X))$
60	57 58 59	syl2anc	$⊢ (φ \land x \in B) \to (x \subseteq X \leftrightarrow (x \in X \lor x = X))$
61		orcom	$⊢ (x \in X \lor x = X) \leftrightarrow (x = X \lor x \in X)$
62	60 61	bitrdi	$⊢ (φ \land x \in B) \to (x \subseteq X \leftrightarrow (x = X \lor x \in X))$
63	62	ifbid	$⊢ (φ \land x \in B) \to if (x \subseteq X, F (x), \emptyset) = if ((x = X \lor x \in X), F (x), \emptyset)$
64	63	mpteq2dva	$⊢ φ \to (x \in B ⟼ if (x \subseteq X, F (x), \emptyset)) = (x \in B ⟼ if ((x = X \lor x \in X), F (x), \emptyset))$
65	64	fveq2d	$⊢ φ \to (A CNF B) ((x \in B ⟼ if (x \subseteq X, F (x), \emptyset))) = (A CNF B) ((x \in B ⟼ if ((x = X \lor x \in X), F (x), \emptyset)))$
66	1 2 3	cantnfs	$⊢ φ \to (F \in S \leftrightarrow (F : B ⟶ A \land {finSupp}_{\emptyset} (F)))$
67	5 66	mpbid	$⊢ φ \to (F : B ⟶ A \land {finSupp}_{\emptyset} (F))$
68	67	simpld	$⊢ φ \to F : B ⟶ A$
69	68	ffvelcdmda	$⊢ (φ \land y \in B) \to F (y) \in A$
70	20	ne0d	$⊢ φ \to A \neq \emptyset$
71		on0eln0	$⊢ A \in On \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
72	2 71	syl	$⊢ φ \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
73	70 72	mpbird	$⊢ φ \to \emptyset \in A$
74	73	adantr	$⊢ (φ \land y \in B) \to \emptyset \in A$
75	69 74	ifcld	$⊢ (φ \land y \in B) \to if (y \in X, F (y), \emptyset) \in A$
76	75	fmpttd	$⊢ φ \to (y \in B ⟼ if (y \in X, F (y), \emptyset)) : B ⟶ A$
77		0ex	$⊢ \emptyset \in V$
78	77	a1i	$⊢ φ \to \emptyset \in V$
79	67	simprd	$⊢ φ \to {finSupp}_{\emptyset} (F)$
80	68 3 78 79	fsuppmptif	$⊢ φ \to {finSupp}_{\emptyset} ((y \in B ⟼ if (y \in X, F (y), \emptyset)))$
81	1 2 3	cantnfs	$⊢ φ \to ((y \in B ⟼ if (y \in X, F (y), \emptyset)) \in S \leftrightarrow ((y \in B ⟼ if (y \in X, F (y), \emptyset)) : B ⟶ A \land {finSupp}_{\emptyset} ((y \in B ⟼ if (y \in X, F (y), \emptyset)))))$
82	76 80 81	mpbir2and	$⊢ φ \to (y \in B ⟼ if (y \in X, F (y), \emptyset)) \in S$
83	68 12	ffvelcdmd	$⊢ φ \to F (X) \in A$
84		eldifn	$⊢ y \in (B ∖ X) \to \neg y \in X$
85	84	adantl	$⊢ (φ \land y \in (B ∖ X)) \to \neg y \in X$
86	85	iffalsed	$⊢ (φ \land y \in (B ∖ X)) \to if (y \in X, F (y), \emptyset) = \emptyset$
87	86 3	suppss2	$⊢ φ \to (y \in B ⟼ if (y \in X, F (y), \emptyset)) supp \emptyset \subseteq X$
88		ifor	$⊢ if ((x = X \lor x \in X), F (x), \emptyset) = if (x = X, F (x), if (x \in X, F (x), \emptyset))$
89		fveq2	$⊢ x = X \to F (x) = F (X)$
90	89	adantl	$⊢ (x \in B \land x = X) \to F (x) = F (X)$
91	90	ifeq1da	$⊢ x \in B \to if (x = X, F (x), (y \in B ⟼ if (y \in X, F (y), \emptyset)) (x)) = if (x = X, F (X), (y \in B ⟼ if (y \in X, F (y), \emptyset)) (x))$
92		eleq1w	$⊢ y = x \to (y \in X \leftrightarrow x \in X)$
93		fveq2	$⊢ y = x \to F (y) = F (x)$
94	92 93	ifbieq1d	$⊢ y = x \to if (y \in X, F (y), \emptyset) = if (x \in X, F (x), \emptyset)$
95		eqid	$⊢ (y \in B ⟼ if (y \in X, F (y), \emptyset)) = (y \in B ⟼ if (y \in X, F (y), \emptyset))$
96		fvex	$⊢ F (x) \in V$
97	96 77	ifex	$⊢ if (x \in X, F (x), \emptyset) \in V$
98	94 95 97	fvmpt	$⊢ x \in B \to (y \in B ⟼ if (y \in X, F (y), \emptyset)) (x) = if (x \in X, F (x), \emptyset)$
99	98	ifeq2d	$⊢ x \in B \to if (x = X, F (x), (y \in B ⟼ if (y \in X, F (y), \emptyset)) (x)) = if (x = X, F (x), if (x \in X, F (x), \emptyset))$
100	91 99	eqtr3d	$⊢ x \in B \to if (x = X, F (X), (y \in B ⟼ if (y \in X, F (y), \emptyset)) (x)) = if (x = X, F (x), if (x \in X, F (x), \emptyset))$
101	88 100	eqtr4id	$⊢ x \in B \to if ((x = X \lor x \in X), F (x), \emptyset) = if (x = X, F (X), (y \in B ⟼ if (y \in X, F (y), \emptyset)) (x))$
102	101	mpteq2ia	$⊢ (x \in B ⟼ if ((x = X \lor x \in X), F (x), \emptyset)) = (x \in B ⟼ if (x = X, F (X), (y \in B ⟼ if (y \in X, F (y), \emptyset)) (x)))$
103	1 2 3 82 12 83 87 102	cantnfp1	$⊢ φ \to ((x \in B ⟼ if ((x = X \lor x \in X), F (x), \emptyset)) \in S \land (A CNF B) ((x \in B ⟼ if ((x = X \lor x \in X), F (x), \emptyset))) = ((A ↑_{𝑜} X) \cdot_{𝑜} F (X)) +_{𝑜} (A CNF B) ((y \in B ⟼ if (y \in X, F (y), \emptyset))))$
104	103	simprd	$⊢ φ \to (A CNF B) ((x \in B ⟼ if ((x = X \lor x \in X), F (x), \emptyset))) = ((A ↑_{𝑜} X) \cdot_{𝑜} F (X)) +_{𝑜} (A CNF B) ((y \in B ⟼ if (y \in X, F (y), \emptyset)))$
105	65 104	eqtrd	$⊢ φ \to (A CNF B) ((x \in B ⟼ if (x \subseteq X, F (x), \emptyset))) = ((A ↑_{𝑜} X) \cdot_{𝑜} F (X)) +_{𝑜} (A CNF B) ((y \in B ⟼ if (y \in X, F (y), \emptyset)))$
106		onelon	$⊢ (A \in On \land F (X) \in A) \to F (X) \in On$
107	2 83 106	syl2anc	$⊢ φ \to F (X) \in On$
108		omsuc	$⊢ (A ↑_{𝑜} X \in On \land F (X) \in On) \to (A ↑_{𝑜} X) \cdot_{𝑜} suc F (X) = ((A ↑_{𝑜} X) \cdot_{𝑜} F (X)) +_{𝑜} (A ↑_{𝑜} X)$
109	16 107 108	syl2anc	$⊢ φ \to (A ↑_{𝑜} X) \cdot_{𝑜} suc F (X) = ((A ↑_{𝑜} X) \cdot_{𝑜} F (X)) +_{𝑜} (A ↑_{𝑜} X)$
110		eloni	$⊢ G (X) \in On \to Ord G (X)$
111	22 110	syl	$⊢ φ \to Ord G (X)$
112	11	simp2d	$⊢ φ \to F (X) \in G (X)$
113		ordsucss	$⊢ Ord G (X) \to (F (X) \in G (X) \to suc F (X) \subseteq G (X))$
114	111 112 113	sylc	$⊢ φ \to suc F (X) \subseteq G (X)$
115		onsuc	$⊢ F (X) \in On \to suc F (X) \in On$
116	107 115	syl	$⊢ φ \to suc F (X) \in On$
117		omwordi	$⊢ (suc F (X) \in On \land G (X) \in On \land A ↑_{𝑜} X \in On) \to (suc F (X) \subseteq G (X) \to (A ↑_{𝑜} X) \cdot_{𝑜} suc F (X) \subseteq (A ↑_{𝑜} X) \cdot_{𝑜} G (X))$
118	116 22 16 117	syl3anc	$⊢ φ \to (suc F (X) \subseteq G (X) \to (A ↑_{𝑜} X) \cdot_{𝑜} suc F (X) \subseteq (A ↑_{𝑜} X) \cdot_{𝑜} G (X))$
119	114 118	mpd	$⊢ φ \to (A ↑_{𝑜} X) \cdot_{𝑜} suc F (X) \subseteq (A ↑_{𝑜} X) \cdot_{𝑜} G (X)$
120	109 119	eqsstrrd	$⊢ φ \to ((A ↑_{𝑜} X) \cdot_{𝑜} F (X)) +_{𝑜} (A ↑_{𝑜} X) \subseteq (A ↑_{𝑜} X) \cdot_{𝑜} G (X)$
121	1 2 3 82 73 14 87	cantnflt2	$⊢ φ \to (A CNF B) ((y \in B ⟼ if (y \in X, F (y), \emptyset))) \in (A ↑_{𝑜} X)$
122		onelon	$⊢ (A ↑_{𝑜} X \in On \land (A CNF B) ((y \in B ⟼ if (y \in X, F (y), \emptyset))) \in (A ↑_{𝑜} X)) \to (A CNF B) ((y \in B ⟼ if (y \in X, F (y), \emptyset))) \in On$
123	16 121 122	syl2anc	$⊢ φ \to (A CNF B) ((y \in B ⟼ if (y \in X, F (y), \emptyset))) \in On$
124		omcl	$⊢ (A ↑_{𝑜} X \in On \land F (X) \in On) \to (A ↑_{𝑜} X) \cdot_{𝑜} F (X) \in On$
125	16 107 124	syl2anc	$⊢ φ \to (A ↑_{𝑜} X) \cdot_{𝑜} F (X) \in On$
126		oaord	$⊢ ((A CNF B) ((y \in B ⟼ if (y \in X, F (y), \emptyset))) \in On \land A ↑_{𝑜} X \in On \land (A ↑_{𝑜} X) \cdot_{𝑜} F (X) \in On) \to ((A CNF B) ((y \in B ⟼ if (y \in X, F (y), \emptyset))) \in (A ↑_{𝑜} X) \leftrightarrow ((A ↑_{𝑜} X) \cdot_{𝑜} F (X)) +_{𝑜} (A CNF B) ((y \in B ⟼ if (y \in X, F (y), \emptyset))) \in (((A ↑_{𝑜} X) \cdot_{𝑜} F (X)) +_{𝑜} (A ↑_{𝑜} X)))$
127	123 16 125 126	syl3anc	$⊢ φ \to ((A CNF B) ((y \in B ⟼ if (y \in X, F (y), \emptyset))) \in (A ↑_{𝑜} X) \leftrightarrow ((A ↑_{𝑜} X) \cdot_{𝑜} F (X)) +_{𝑜} (A CNF B) ((y \in B ⟼ if (y \in X, F (y), \emptyset))) \in (((A ↑_{𝑜} X) \cdot_{𝑜} F (X)) +_{𝑜} (A ↑_{𝑜} X)))$
128	121 127	mpbid	$⊢ φ \to ((A ↑_{𝑜} X) \cdot_{𝑜} F (X)) +_{𝑜} (A CNF B) ((y \in B ⟼ if (y \in X, F (y), \emptyset))) \in (((A ↑_{𝑜} X) \cdot_{𝑜} F (X)) +_{𝑜} (A ↑_{𝑜} X))$
129	120 128	sseldd	$⊢ φ \to ((A ↑_{𝑜} X) \cdot_{𝑜} F (X)) +_{𝑜} (A CNF B) ((y \in B ⟼ if (y \in X, F (y), \emptyset))) \in ((A ↑_{𝑜} X) \cdot_{𝑜} G (X))$
130	105 129	eqeltrd	$⊢ φ \to (A CNF B) ((x \in B ⟼ if (x \subseteq X, F (x), \emptyset))) \in ((A ↑_{𝑜} X) \cdot_{𝑜} G (X))$
131	54 130	sseldd	$⊢ φ \to (A CNF B) ((x \in B ⟼ if (x \subseteq X, F (x), \emptyset))) \in H (suc O^{-1} (X))$

Metamath Proof Explorer

Theorem cantnflem1d

Proof