cantnfp1lem2

Description: Lemma for cantnfp1 . (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 30-Jun-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)$
Assertion	cantnfp1lem2	$⊢ φ \to dom O = suc ⋃ dom O$

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		iftrue	$⊢ t = X \to if (t = X, Y, G (t)) = Y$
12	8 11 5 6	fvmptd3	$⊢ φ \to F (X) = Y$
13	9	ne0d	$⊢ φ \to Y \neq \emptyset$
14	12 13	eqnetrd	$⊢ φ \to F (X) \neq \emptyset$
15	6	adantr	$⊢ (φ \land t \in B) \to Y \in A$
16	1 2 3	cantnfs	$⊢ φ \to (G \in S \leftrightarrow (G : B ⟶ A \land {finSupp}_{\emptyset} (G)))$
17	4 16	mpbid	$⊢ φ \to (G : B ⟶ A \land {finSupp}_{\emptyset} (G))$
18	17	simpld	$⊢ φ \to G : B ⟶ A$
19	18	ffvelcdmda	$⊢ (φ \land t \in B) \to G (t) \in A$
20	15 19	ifcld	$⊢ (φ \land t \in B) \to if (t = X, Y, G (t)) \in A$
21	20 8	fmptd	$⊢ φ \to F : B ⟶ A$
22	21	ffnd	$⊢ φ \to F Fn B$
23	9	elexd	$⊢ φ \to \emptyset \in V$
24		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))$
25	22 3 23 24	syl3anc	$⊢ φ \to (X \in {supp}_{\emptyset} (F) \leftrightarrow (X \in B \land F (X) \neq \emptyset))$
26	5 14 25	mpbir2and	$⊢ φ \to X \in {supp}_{\emptyset} (F)$
27		n0i	$⊢ X \in {supp}_{\emptyset} (F) \to \neg F supp \emptyset = \emptyset$
28	26 27	syl	$⊢ φ \to \neg F supp \emptyset = \emptyset$
29		ovexd	$⊢ φ \to F supp \emptyset \in V$
30	1 2 3 4 5 6 7 8	cantnfp1lem1	$⊢ φ \to F \in S$
31	1 2 3 10 30	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (F) \land dom O \in ω)$
32	31	simpld	$⊢ φ \to E We {supp}_{\emptyset} (F)$
33	10	oien	$⊢ (F supp \emptyset \in V \land E We {supp}_{\emptyset} (F)) \to dom O \approx {supp}_{\emptyset} (F)$
34	29 32 33	syl2anc	$⊢ φ \to dom O \approx {supp}_{\emptyset} (F)$
35		breq1	$⊢ dom O = \emptyset \to (dom O \approx {supp}_{\emptyset} (F) \leftrightarrow \emptyset \approx {supp}_{\emptyset} (F))$
36		ensymb	$⊢ \emptyset \approx {supp}_{\emptyset} (F) \leftrightarrow {supp}_{\emptyset} (F) \approx \emptyset$
37		en0	$⊢ {supp}_{\emptyset} (F) \approx \emptyset \leftrightarrow F supp \emptyset = \emptyset$
38	36 37	bitri	$⊢ \emptyset \approx {supp}_{\emptyset} (F) \leftrightarrow F supp \emptyset = \emptyset$
39	35 38	bitrdi	$⊢ dom O = \emptyset \to (dom O \approx {supp}_{\emptyset} (F) \leftrightarrow F supp \emptyset = \emptyset)$
40	34 39	syl5ibcom	$⊢ φ \to (dom O = \emptyset \to F supp \emptyset = \emptyset)$
41	28 40	mtod	$⊢ φ \to \neg dom O = \emptyset$
42	31	simprd	$⊢ φ \to dom O \in ω$
43		nnlim	$⊢ dom O \in ω \to \neg Lim dom O$
44	42 43	syl	$⊢ φ \to \neg Lim dom O$
45		ioran	$⊢ \neg (dom O = \emptyset \lor Lim dom O) \leftrightarrow (\neg dom O = \emptyset \land \neg Lim dom O)$
46	41 44 45	sylanbrc	$⊢ φ \to \neg (dom O = \emptyset \lor Lim dom O)$
47		nnord	$⊢ dom O \in ω \to Ord dom O$
48		unizlim	$⊢ Ord dom O \to (dom O = ⋃ dom O \leftrightarrow (dom O = \emptyset \lor Lim dom O))$
49	42 47 48	3syl	$⊢ φ \to (dom O = ⋃ dom O \leftrightarrow (dom O = \emptyset \lor Lim dom O))$
50	46 49	mtbird	$⊢ φ \to \neg dom O = ⋃ dom O$
51		orduniorsuc	$⊢ Ord dom O \to (dom O = ⋃ dom O \lor dom O = suc ⋃ dom O)$
52	42 47 51	3syl	$⊢ φ \to (dom O = ⋃ dom O \lor dom O = suc ⋃ dom O)$
53	52	ord	$⊢ φ \to (\neg dom O = ⋃ dom O \to dom O = suc ⋃ dom O)$
54	50 53	mpd	$⊢ φ \to dom O = suc ⋃ dom O$

Metamath Proof Explorer

Theorem cantnfp1lem2

Proof