cnfcom2lem

Description: Lemma for cnfcom2 . (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 3-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)$
	cnfcom2.1	$⊢ φ \to \emptyset \in B$
Assertion	cnfcom2lem	$⊢ φ \to dom G = suc ⋃ dom G$

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		cnfcom2.1	$⊢ φ \to \emptyset \in B$
12		n0i	$⊢ \emptyset \in B \to \neg B = \emptyset$
13	11 12	syl	$⊢ φ \to \neg B = \emptyset$
14		omelon	$⊢ ω \in On$
15	14	a1i	$⊢ φ \to ω \in On$
16	1 15 2	cantnff1o	$⊢ φ \to (ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A$
17		f1ocnv	$⊢ (ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A \underset{1-1 onto}{⟶} S$
18		f1of	$⊢ {(ω CNF A)}^{-1} : ω ↑_{𝑜} A \underset{1-1 onto}{⟶} S \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A ⟶ S$
19	16 17 18	3syl	$⊢ φ \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A ⟶ S$
20	19 3	ffvelrnd	$⊢ φ \to {(ω CNF A)}^{-1} (B) \in S$
21	4 20	eqeltrid	$⊢ φ \to F \in S$
22	1 15 2	cantnfs	$⊢ φ \to (F \in S \leftrightarrow (F : A ⟶ ω \land {finSupp}_{\emptyset} (F)))$
23	21 22	mpbid	$⊢ φ \to (F : A ⟶ ω \land {finSupp}_{\emptyset} (F))$
24	23	simpld	$⊢ φ \to F : A ⟶ ω$
25	24	adantr	$⊢ (φ \land dom G = \emptyset) \to F : A ⟶ ω$
26	25	feqmptd	$⊢ (φ \land dom G = \emptyset) \to F = (x \in A ⟼ F (x))$
27		dif0	$⊢ A ∖ \emptyset = A$
28	27	eleq2i	$⊢ x \in (A ∖ \emptyset) \leftrightarrow x \in A$
29		simpr	$⊢ (φ \land dom G = \emptyset) \to dom G = \emptyset$
30		ovexd	$⊢ φ \to F supp \emptyset \in V$
31	1 15 2 5 21	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (F) \land dom G \in ω)$
32	31	simpld	$⊢ φ \to E We {supp}_{\emptyset} (F)$
33	5	oien	$⊢ (F supp \emptyset \in V \land E We {supp}_{\emptyset} (F)) \to dom G \approx {supp}_{\emptyset} (F)$
34	30 32 33	syl2anc	$⊢ φ \to dom G \approx {supp}_{\emptyset} (F)$
35	34	adantr	$⊢ (φ \land dom G = \emptyset) \to dom G \approx {supp}_{\emptyset} (F)$
36	29 35	eqbrtrrd	$⊢ (φ \land dom G = \emptyset) \to \emptyset \approx {supp}_{\emptyset} (F)$
37	36	ensymd	$⊢ (φ \land dom G = \emptyset) \to {supp}_{\emptyset} (F) \approx \emptyset$
38		en0	$⊢ {supp}_{\emptyset} (F) \approx \emptyset \leftrightarrow F supp \emptyset = \emptyset$
39	37 38	sylib	$⊢ (φ \land dom G = \emptyset) \to F supp \emptyset = \emptyset$
40		ss0b	$⊢ F supp \emptyset \subseteq \emptyset \leftrightarrow F supp \emptyset = \emptyset$
41	39 40	sylibr	$⊢ (φ \land dom G = \emptyset) \to F supp \emptyset \subseteq \emptyset$
42	2	adantr	$⊢ (φ \land dom G = \emptyset) \to A \in On$
43		0ex	$⊢ \emptyset \in V$
44	43	a1i	$⊢ (φ \land dom G = \emptyset) \to \emptyset \in V$
45	25 41 42 44	suppssr	$⊢ ((φ \land dom G = \emptyset) \land x \in (A ∖ \emptyset)) \to F (x) = \emptyset$
46	28 45	sylan2br	$⊢ ((φ \land dom G = \emptyset) \land x \in A) \to F (x) = \emptyset$
47	46	mpteq2dva	$⊢ (φ \land dom G = \emptyset) \to (x \in A ⟼ F (x)) = (x \in A ⟼ \emptyset)$
48	26 47	eqtrd	$⊢ (φ \land dom G = \emptyset) \to F = (x \in A ⟼ \emptyset)$
49		fconstmpt	$⊢ A \times \{\emptyset\} = (x \in A ⟼ \emptyset)$
50	48 49	eqtr4di	$⊢ (φ \land dom G = \emptyset) \to F = A \times \{\emptyset\}$
51	50	fveq2d	$⊢ (φ \land dom G = \emptyset) \to (ω CNF A) (F) = (ω CNF A) (A \times \{\emptyset\})$
52	4	fveq2i	$⊢ (ω CNF A) (F) = (ω CNF A) ({(ω CNF A)}^{-1} (B))$
53		f1ocnvfv2	$⊢ ((ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A \land B \in (ω ↑_{𝑜} A)) \to (ω CNF A) ({(ω CNF A)}^{-1} (B)) = B$
54	16 3 53	syl2anc	$⊢ φ \to (ω CNF A) ({(ω CNF A)}^{-1} (B)) = B$
55	52 54	syl5eq	$⊢ φ \to (ω CNF A) (F) = B$
56	55	adantr	$⊢ (φ \land dom G = \emptyset) \to (ω CNF A) (F) = B$
57		peano1	$⊢ \emptyset \in ω$
58	57	a1i	$⊢ φ \to \emptyset \in ω$
59	1 15 2 58	cantnf0	$⊢ φ \to (ω CNF A) (A \times \{\emptyset\}) = \emptyset$
60	59	adantr	$⊢ (φ \land dom G = \emptyset) \to (ω CNF A) (A \times \{\emptyset\}) = \emptyset$
61	51 56 60	3eqtr3d	$⊢ (φ \land dom G = \emptyset) \to B = \emptyset$
62	13 61	mtand	$⊢ φ \to \neg dom G = \emptyset$
63		nnlim	$⊢ dom G \in ω \to \neg Lim dom G$
64	31 63	simpl2im	$⊢ φ \to \neg Lim dom G$
65		ioran	$⊢ \neg (dom G = \emptyset \lor Lim dom G) \leftrightarrow (\neg dom G = \emptyset \land \neg Lim dom G)$
66	62 64 65	sylanbrc	$⊢ φ \to \neg (dom G = \emptyset \lor Lim dom G)$
67	5	oicl	$⊢ Ord dom G$
68		unizlim	$⊢ Ord dom G \to (dom G = ⋃ dom G \leftrightarrow (dom G = \emptyset \lor Lim dom G))$
69	67 68	ax-mp	$⊢ dom G = ⋃ dom G \leftrightarrow (dom G = \emptyset \lor Lim dom G)$
70	66 69	sylnibr	$⊢ φ \to \neg dom G = ⋃ dom G$
71		orduniorsuc	$⊢ Ord dom G \to (dom G = ⋃ dom G \lor dom G = suc ⋃ dom G)$
72	67 71	mp1i	$⊢ φ \to (dom G = ⋃ dom G \lor dom G = suc ⋃ dom G)$
73	72	ord	$⊢ φ \to (\neg dom G = ⋃ dom G \to dom G = suc ⋃ dom G)$
74	70 73	mpd	$⊢ φ \to dom G = suc ⋃ dom G$

Metamath Proof Explorer

Theorem cnfcom2lem

Proof