cnfcom3lem

Description: Lemma for cnfcom3 . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 4-Jul-2019)

	Ref	Expression
Hypotheses	cnfcom.s	$⊢ S = dom (ω CNF A)$
	cnfcom.a	$⊢ φ \to A \in On$
	cnfcom.b	$⊢ φ \to B \in (ω ↑_{𝑜} A)$
	cnfcom.f	$⊢ F = {(ω CNF A)}^{-1} (B)$
	cnfcom.g	$⊢ G = OrdIso (E, F supp \emptyset)$
	cnfcom.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ M +_{𝑜} z), \emptyset)$
	cnfcom.t	$⊢ T = {seq}_{ω} ((k \in V, f \in V ⟼ K), \emptyset)$
	cnfcom.m	$⊢ M = (ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))$
	cnfcom.k	$⊢ K = (x \in M ⟼ dom f +_{𝑜} x) \cup {(x \in dom f ⟼ M +_{𝑜} x)}^{-1}$
	cnfcom.w	$⊢ W = G (⋃ dom G)$
	cnfcom3.1	$⊢ φ \to ω \subseteq B$
Assertion	cnfcom3lem	$⊢ φ \to W \in (On ∖ 1_{𝑜})$

Proof

Step	Hyp	Ref	Expression
1		cnfcom.s	$⊢ S = dom (ω CNF A)$
2		cnfcom.a	$⊢ φ \to A \in On$
3		cnfcom.b	$⊢ φ \to B \in (ω ↑_{𝑜} A)$
4		cnfcom.f	$⊢ F = {(ω CNF A)}^{-1} (B)$
5		cnfcom.g	$⊢ G = OrdIso (E, F supp \emptyset)$
6		cnfcom.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ M +_{𝑜} z), \emptyset)$
7		cnfcom.t	$⊢ T = {seq}_{ω} ((k \in V, f \in V ⟼ K), \emptyset)$
8		cnfcom.m	$⊢ M = (ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))$
9		cnfcom.k	$⊢ K = (x \in M ⟼ dom f +_{𝑜} x) \cup {(x \in dom f ⟼ M +_{𝑜} x)}^{-1}$
10		cnfcom.w	$⊢ W = G (⋃ dom G)$
11		cnfcom3.1	$⊢ φ \to ω \subseteq B$
12		suppssdm	$⊢ F supp \emptyset \subseteq dom F$
13		omelon	$⊢ ω \in On$
14	13	a1i	$⊢ φ \to ω \in On$
15	1 14 2	cantnff1o	$⊢ φ \to (ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A$
16		f1ocnv	$⊢ (ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A \underset{1-1 onto}{⟶} S$
17		f1of	$⊢ {(ω CNF A)}^{-1} : ω ↑_{𝑜} A \underset{1-1 onto}{⟶} S \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A ⟶ S$
18	15 16 17	3syl	$⊢ φ \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A ⟶ S$
19	18 3	ffvelrnd	$⊢ φ \to {(ω CNF A)}^{-1} (B) \in S$
20	4 19	eqeltrid	$⊢ φ \to F \in S$
21	1 14 2	cantnfs	$⊢ φ \to (F \in S \leftrightarrow (F : A ⟶ ω \land {finSupp}_{\emptyset} (F)))$
22	20 21	mpbid	$⊢ φ \to (F : A ⟶ ω \land {finSupp}_{\emptyset} (F))$
23	22	simpld	$⊢ φ \to F : A ⟶ ω$
24	12 23	fssdm	$⊢ φ \to F supp \emptyset \subseteq A$
25		ovex	$⊢ F supp \emptyset \in V$
26	5	oion	$⊢ F supp \emptyset \in V \to dom G \in On$
27	25 26	ax-mp	$⊢ dom G \in On$
28	27	elexi	$⊢ dom G \in V$
29	28	uniex	$⊢ ⋃ dom G \in V$
30	29	sucid	$⊢ ⋃ dom G \in suc ⋃ dom G$
31		peano1	$⊢ \emptyset \in ω$
32	31	a1i	$⊢ φ \to \emptyset \in ω$
33	11 32	sseldd	$⊢ φ \to \emptyset \in B$
34	1 2 3 4 5 6 7 8 9 10 33	cnfcom2lem	$⊢ φ \to dom G = suc ⋃ dom G$
35	30 34	eleqtrrid	$⊢ φ \to ⋃ dom G \in dom G$
36	5	oif	$⊢ G : dom G ⟶ F supp \emptyset$
37	36	ffvelrni	$⊢ ⋃ dom G \in dom G \to G (⋃ dom G) \in {supp}_{\emptyset} (F)$
38	35 37	syl	$⊢ φ \to G (⋃ dom G) \in {supp}_{\emptyset} (F)$
39	24 38	sseldd	$⊢ φ \to G (⋃ dom G) \in A$
40		onelon	$⊢ (A \in On \land G (⋃ dom G) \in A) \to G (⋃ dom G) \in On$
41	2 39 40	syl2anc	$⊢ φ \to G (⋃ dom G) \in On$
42	10 41	eqeltrid	$⊢ φ \to W \in On$
43		oecl	$⊢ (ω \in On \land A \in On) \to ω ↑_{𝑜} A \in On$
44	13 2 43	sylancr	$⊢ φ \to ω ↑_{𝑜} A \in On$
45		onelon	$⊢ (ω ↑_{𝑜} A \in On \land B \in (ω ↑_{𝑜} A)) \to B \in On$
46	44 3 45	syl2anc	$⊢ φ \to B \in On$
47		ontri1	$⊢ (ω \in On \land B \in On) \to (ω \subseteq B \leftrightarrow \neg B \in ω)$
48	13 46 47	sylancr	$⊢ φ \to (ω \subseteq B \leftrightarrow \neg B \in ω)$
49	11 48	mpbid	$⊢ φ \to \neg B \in ω$
50	4	fveq2i	$⊢ (ω CNF A) (F) = (ω CNF A) ({(ω CNF A)}^{-1} (B))$
51		f1ocnvfv2	$⊢ ((ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A \land B \in (ω ↑_{𝑜} A)) \to (ω CNF A) ({(ω CNF A)}^{-1} (B)) = B$
52	15 3 51	syl2anc	$⊢ φ \to (ω CNF A) ({(ω CNF A)}^{-1} (B)) = B$
53	50 52	eqtrid	$⊢ φ \to (ω CNF A) (F) = B$
54	53	adantr	$⊢ (φ \land W = \emptyset) \to (ω CNF A) (F) = B$
55	13	a1i	$⊢ (φ \land W = \emptyset) \to ω \in On$
56	2	adantr	$⊢ (φ \land W = \emptyset) \to A \in On$
57	20	adantr	$⊢ (φ \land W = \emptyset) \to F \in S$
58	31	a1i	$⊢ (φ \land W = \emptyset) \to \emptyset \in ω$
59		1on	$⊢ 1_{𝑜} \in On$
60	59	a1i	$⊢ (φ \land W = \emptyset) \to 1_{𝑜} \in On$
61		ovexd	$⊢ φ \to F supp \emptyset \in V$
62	1 14 2 5 20	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (F) \land dom G \in ω)$
63	62	simpld	$⊢ φ \to E We {supp}_{\emptyset} (F)$
64	5	oiiso	$⊢ (F supp \emptyset \in V \land E We {supp}_{\emptyset} (F)) \to G {Isom}_{E, E} (dom G, F supp \emptyset)$
65	61 63 64	syl2anc	$⊢ φ \to G {Isom}_{E, E} (dom G, F supp \emptyset)$
66	65	ad2antrr	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to G {Isom}_{E, E} (dom G, F supp \emptyset)$
67		isof1o	$⊢ G {Isom}_{E, E} (dom G, F supp \emptyset) \to G : dom G \underset{1-1 onto}{⟶} F supp \emptyset$
68	66 67	syl	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to G : dom G \underset{1-1 onto}{⟶} F supp \emptyset$
69		f1ocnv	$⊢ G : dom G \underset{1-1 onto}{⟶} F supp \emptyset \to G^{-1} : F supp \emptyset \underset{1-1 onto}{⟶} dom G$
70		f1of	$⊢ G^{-1} : F supp \emptyset \underset{1-1 onto}{⟶} dom G \to G^{-1} : F supp \emptyset ⟶ dom G$
71	68 69 70	3syl	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to G^{-1} : F supp \emptyset ⟶ dom G$
72		ffvelrn	$⊢ (G^{-1} : F supp \emptyset ⟶ dom G \land x \in {supp}_{\emptyset} (F)) \to G^{-1} (x) \in dom G$
73	71 72	sylancom	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to G^{-1} (x) \in dom G$
74		elssuni	$⊢ G^{-1} (x) \in dom G \to G^{-1} (x) \subseteq ⋃ dom G$
75	73 74	syl	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to G^{-1} (x) \subseteq ⋃ dom G$
76		onelon	$⊢ (dom G \in On \land G^{-1} (x) \in dom G) \to G^{-1} (x) \in On$
77	27 73 76	sylancr	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to G^{-1} (x) \in On$
78		onuni	$⊢ dom G \in On \to ⋃ dom G \in On$
79	27 78	ax-mp	$⊢ ⋃ dom G \in On$
80		ontri1	$⊢ (G^{-1} (x) \in On \land ⋃ dom G \in On) \to (G^{-1} (x) \subseteq ⋃ dom G \leftrightarrow \neg ⋃ dom G \in G^{-1} (x))$
81	77 79 80	sylancl	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to (G^{-1} (x) \subseteq ⋃ dom G \leftrightarrow \neg ⋃ dom G \in G^{-1} (x))$
82	75 81	mpbid	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to \neg ⋃ dom G \in G^{-1} (x)$
83	35	ad2antrr	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to ⋃ dom G \in dom G$
84		isorel	$⊢ (G {Isom}_{E, E} (dom G, F supp \emptyset) \land (⋃ dom G \in dom G \land G^{-1} (x) \in dom G)) \to (⋃ dom G E G^{-1} (x) \leftrightarrow G (⋃ dom G) E G (G^{-1} (x)))$
85	66 83 73 84	syl12anc	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to (⋃ dom G E G^{-1} (x) \leftrightarrow G (⋃ dom G) E G (G^{-1} (x)))$
86		fvex	$⊢ G^{-1} (x) \in V$
87	86	epeli	$⊢ ⋃ dom G E G^{-1} (x) \leftrightarrow ⋃ dom G \in G^{-1} (x)$
88	10	breq1i	$⊢ W E G (G^{-1} (x)) \leftrightarrow G (⋃ dom G) E G (G^{-1} (x))$
89		fvex	$⊢ G (G^{-1} (x)) \in V$
90	89	epeli	$⊢ W E G (G^{-1} (x)) \leftrightarrow W \in G (G^{-1} (x))$
91	88 90	bitr3i	$⊢ G (⋃ dom G) E G (G^{-1} (x)) \leftrightarrow W \in G (G^{-1} (x))$
92	85 87 91	3bitr3g	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to (⋃ dom G \in G^{-1} (x) \leftrightarrow W \in G (G^{-1} (x)))$
93		simplr	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to W = \emptyset$
94		f1ocnvfv2	$⊢ (G : dom G \underset{1-1 onto}{⟶} F supp \emptyset \land x \in {supp}_{\emptyset} (F)) \to G (G^{-1} (x)) = x$
95	68 94	sylancom	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to G (G^{-1} (x)) = x$
96	93 95	eleq12d	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to (W \in G (G^{-1} (x)) \leftrightarrow \emptyset \in x)$
97	92 96	bitrd	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to (⋃ dom G \in G^{-1} (x) \leftrightarrow \emptyset \in x)$
98	82 97	mtbid	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to \neg \emptyset \in x$
99		onss	$⊢ A \in On \to A \subseteq On$
100	2 99	syl	$⊢ φ \to A \subseteq On$
101	24 100	sstrd	$⊢ φ \to F supp \emptyset \subseteq On$
102	101	adantr	$⊢ (φ \land W = \emptyset) \to F supp \emptyset \subseteq On$
103	102	sselda	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to x \in On$
104		on0eqel	$⊢ x \in On \to (x = \emptyset \lor \emptyset \in x)$
105	103 104	syl	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to (x = \emptyset \lor \emptyset \in x)$
106	105	ord	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to (\neg x = \emptyset \to \emptyset \in x)$
107	98 106	mt3d	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to x = \emptyset$
108		el1o	$⊢ x \in 1_{𝑜} \leftrightarrow x = \emptyset$
109	107 108	sylibr	$⊢ ((φ \land W = \emptyset) \land x \in {supp}_{\emptyset} (F)) \to x \in 1_{𝑜}$
110	109	ex	$⊢ (φ \land W = \emptyset) \to (x \in {supp}_{\emptyset} (F) \to x \in 1_{𝑜})$
111	110	ssrdv	$⊢ (φ \land W = \emptyset) \to F supp \emptyset \subseteq 1_{𝑜}$
112	1 55 56 57 58 60 111	cantnflt2	$⊢ (φ \land W = \emptyset) \to (ω CNF A) (F) \in (ω ↑_{𝑜} 1_{𝑜})$
113		oe1	$⊢ ω \in On \to ω ↑_{𝑜} 1_{𝑜} = ω$
114	13 113	ax-mp	$⊢ ω ↑_{𝑜} 1_{𝑜} = ω$
115	112 114	eleqtrdi	$⊢ (φ \land W = \emptyset) \to (ω CNF A) (F) \in ω$
116	54 115	eqeltrrd	$⊢ (φ \land W = \emptyset) \to B \in ω$
117	116	ex	$⊢ φ \to (W = \emptyset \to B \in ω)$
118	117	necon3bd	$⊢ φ \to (\neg B \in ω \to W \neq \emptyset)$
119	49 118	mpd	$⊢ φ \to W \neq \emptyset$
120		dif1o	$⊢ W \in (On ∖ 1_{𝑜}) \leftrightarrow (W \in On \land W \neq \emptyset)$
121	42 119 120	sylanbrc	$⊢ φ \to W \in (On ∖ 1_{𝑜})$

Metamath Proof Explorer

Theorem cnfcom3lem

Proof