cantnfcl

Description: Basic properties of the order isomorphism G used later. The support of an F e. S is a finite subset of A , so it is well-ordered by _E and the order isomorphism has domain a finite ordinal. (Contributed by Mario Carneiro, 25-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$
Assertion	cantnfcl	$⊢ φ \to (E We {supp}_{\emptyset} (F) \land dom G \in ω)$

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		suppssdm	$⊢ F supp \emptyset \subseteq dom F$
7	1 2 3	cantnfs	$⊢ φ \to (F \in S \leftrightarrow (F : B ⟶ A \land {finSupp}_{\emptyset} (F)))$
8	5 7	mpbid	$⊢ φ \to (F : B ⟶ A \land {finSupp}_{\emptyset} (F))$
9	8	simpld	$⊢ φ \to F : B ⟶ A$
10	6 9	fssdm	$⊢ φ \to F supp \emptyset \subseteq B$
11		onss	$⊢ B \in On \to B \subseteq On$
12	3 11	syl	$⊢ φ \to B \subseteq On$
13	10 12	sstrd	$⊢ φ \to F supp \emptyset \subseteq On$
14		epweon	$⊢ E We On$
15		wess	$⊢ F supp \emptyset \subseteq On \to (E We On \to E We {supp}_{\emptyset} (F))$
16	13 14 15	mpisyl	$⊢ φ \to E We {supp}_{\emptyset} (F)$
17		ovexd	$⊢ φ \to F supp \emptyset \in V$
18	4	oion	$⊢ F supp \emptyset \in V \to dom G \in On$
19	17 18	syl	$⊢ φ \to dom G \in On$
20	8	simprd	$⊢ φ \to {finSupp}_{\emptyset} (F)$
21	20	fsuppimpd	$⊢ φ \to F supp \emptyset \in Fin$
22	4	oien	$⊢ (F supp \emptyset \in V \land E We {supp}_{\emptyset} (F)) \to dom G \approx {supp}_{\emptyset} (F)$
23	17 16 22	syl2anc	$⊢ φ \to dom G \approx {supp}_{\emptyset} (F)$
24		enfii	$⊢ (F supp \emptyset \in Fin \land dom G \approx {supp}_{\emptyset} (F)) \to dom G \in Fin$
25	21 23 24	syl2anc	$⊢ φ \to dom G \in Fin$
26	19 25	elind	$⊢ φ \to dom G \in (On \cap Fin)$
27		onfin2	$⊢ ω = On \cap Fin$
28	26 27	eleqtrrdi	$⊢ φ \to dom G \in ω$
29	16 28	jca	$⊢ φ \to (E We {supp}_{\emptyset} (F) \land dom G \in ω)$

Metamath Proof Explorer

Theorem cantnfcl

Proof