Theorem 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	|- ( ph -> A e. On )
	cantnfs.b	|- ( ph -> B e. On )
	cantnfcl.g	|- G = OrdIso ( _E , ( F supp (/) ) )
	cantnfcl.f	|- ( ph -> F e. S )
Assertion	cantnfcl	|- ( ph -> ( _E We ( F supp (/) ) /\ dom G e. _om ) )

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	|- S = dom ( A CNF B )
2		cantnfs.a	|- ( ph -> A e. On )
3		cantnfs.b	|- ( ph -> B e. On )
4		cantnfcl.g	|- G = OrdIso ( _E , ( F supp (/) ) )
5		cantnfcl.f	|- ( ph -> F e. S )
6		suppssdm	|- ( F supp (/) ) C_ dom F
7	1 2 3	cantnfs	|- ( ph -> ( F e. S <-> ( F : B --> A /\ F finSupp (/) ) ) )
8	5 7	mpbid	|- ( ph -> ( F : B --> A /\ F finSupp (/) ) )
9	8	simpld	|- ( ph -> F : B --> A )
10	6 9	fssdm	|- ( ph -> ( F supp (/) ) C_ B )
11		onss	|- ( B e. On -> B C_ On )
12	3 11	syl	|- ( ph -> B C_ On )
13	10 12	sstrd	|- ( ph -> ( F supp (/) ) C_ On )
14		epweon	|- _E We On
15		wess	|- ( ( F supp (/) ) C_ On -> ( _E We On -> _E We ( F supp (/) ) ) )
16	13 14 15	mpisyl	|- ( ph -> _E We ( F supp (/) ) )
17		ovexd	|- ( ph -> ( F supp (/) ) e. _V )
18	4	oion	|- ( ( F supp (/) ) e. _V -> dom G e. On )
19	17 18	syl	|- ( ph -> dom G e. On )
20	8	simprd	|- ( ph -> F finSupp (/) )
21	20	fsuppimpd	|- ( ph -> ( F supp (/) ) e. Fin )
22	4	oien	|- ( ( ( F supp (/) ) e. _V /\ _E We ( F supp (/) ) ) -> dom G ~~ ( F supp (/) ) )
23	17 16 22	syl2anc	|- ( ph -> dom G ~~ ( F supp (/) ) )
24		enfii	|- ( ( ( F supp (/) ) e. Fin /\ dom G ~~ ( F supp (/) ) ) -> dom G e. Fin )
25	21 23 24	syl2anc	|- ( ph -> dom G e. Fin )
26	19 25	elind	|- ( ph -> dom G e. ( On i^i Fin ) )
27		onfin2	|- _om = ( On i^i Fin )
28	26 27	eleqtrrdi	|- ( ph -> dom G e. _om )
29	16 28	jca	|- ( ph -> ( _E We ( F supp (/) ) /\ dom G e. _om ) )