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	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
	cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
	cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
	cantnfcl.g	⊢ 𝐺 = OrdIso ( E , ( 𝐹 supp ∅ ) )
	cantnfcl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
Assertion	cantnfcl	⊢ ( 𝜑 → ( E We ( 𝐹 supp ∅ ) ∧ dom 𝐺 ∈ ω ) )

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2		cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
3		cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
4		cantnfcl.g	⊢ 𝐺 = OrdIso ( E , ( 𝐹 supp ∅ ) )
5		cantnfcl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
6		suppssdm	⊢ ( 𝐹 supp ∅ ) ⊆ dom 𝐹
7	1 2 3	cantnfs	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) ) )
8	5 7	mpbid	⊢ ( 𝜑 → ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) )
9	8	simpld	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐴 )
10	6 9	fssdm	⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ 𝐵 )
11		onss	⊢ ( 𝐵 ∈ On → 𝐵 ⊆ On )
12	3 11	syl	⊢ ( 𝜑 → 𝐵 ⊆ On )
13	10 12	sstrd	⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ On )
14		epweon	⊢ E We On
15		wess	⊢ ( ( 𝐹 supp ∅ ) ⊆ On → ( E We On → E We ( 𝐹 supp ∅ ) ) )
16	13 14 15	mpisyl	⊢ ( 𝜑 → E We ( 𝐹 supp ∅ ) )
17		ovexd	⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ∈ V )
18	4	oion	⊢ ( ( 𝐹 supp ∅ ) ∈ V → dom 𝐺 ∈ On )
19	17 18	syl	⊢ ( 𝜑 → dom 𝐺 ∈ On )
20	8	simprd	⊢ ( 𝜑 → 𝐹 finSupp ∅ )
21	20	fsuppimpd	⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ∈ Fin )
22	4	oien	⊢ ( ( ( 𝐹 supp ∅ ) ∈ V ∧ E We ( 𝐹 supp ∅ ) ) → dom 𝐺 ≈ ( 𝐹 supp ∅ ) )
23	17 16 22	syl2anc	⊢ ( 𝜑 → dom 𝐺 ≈ ( 𝐹 supp ∅ ) )
24		enfii	⊢ ( ( ( 𝐹 supp ∅ ) ∈ Fin ∧ dom 𝐺 ≈ ( 𝐹 supp ∅ ) ) → dom 𝐺 ∈ Fin )
25	21 23 24	syl2anc	⊢ ( 𝜑 → dom 𝐺 ∈ Fin )
26	19 25	elind	⊢ ( 𝜑 → dom 𝐺 ∈ ( On ∩ Fin ) )
27		onfin2	⊢ ω = ( On ∩ Fin )
28	26 27	eleqtrrdi	⊢ ( 𝜑 → dom 𝐺 ∈ ω )
29	16 28	jca	⊢ ( 𝜑 → ( E We ( 𝐹 supp ∅ ) ∧ dom 𝐺 ∈ ω ) )

Metamath Proof Explorer

Theorem cantnfcl

Proof