Metamath Proof Explorer

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 ⊢ φ → A ∈ On
cantnfs.b ⊢ φ → B ∈ On
cantnfcl.g ⊢ G = OrdIso E F supp ∅
cantnfcl.f ⊢ φ → F ∈ S
Assertion cantnfcl ⊢ φ → E We supp ∅⁡ F ∧ dom ⁡ G ∈ ω

Proof

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