Metamath Proof Explorer

Theorem cantnflt2

Description: An upper bound on the CNF function. (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 29-Jun-2019)

Ref Expression
Hypotheses cantnfs.s ⊢ S = dom ⁡ A CNF B
cantnfs.a ⊢ φ → A ∈ On
cantnfs.b ⊢ φ → B ∈ On
cantnflt2.f ⊢ φ → F ∈ S
cantnflt2.a ⊢ φ → ∅ ∈ A
cantnflt2.c ⊢ φ → C ∈ On
cantnflt2.s ⊢ φ → F supp ∅ ⊆ C
Assertion cantnflt2 ⊢ φ → A CNF B ⁡ F ∈ A ↑ 𝑜 C

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ S = dom ⁡ A CNF B
2 cantnfs.a ⊢ φ → A ∈ On
3 cantnfs.b ⊢ φ → B ∈ On
4 cantnflt2.f ⊢ φ → F ∈ S
5 cantnflt2.a ⊢ φ → ∅ ∈ A
6 cantnflt2.c ⊢ φ → C ∈ On
7 cantnflt2.s ⊢ φ → F supp ∅ ⊆ C
8 eqid ⊢ OrdIso E F supp ∅ = OrdIso E F supp ∅
9 eqid ⊢ seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 OrdIso E F supp ∅ ⁡ k ⋅ 𝑜 F ⁡ OrdIso E F supp ∅ ⁡ k + 𝑜 z ∅ = seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 OrdIso E F supp ∅ ⁡ k ⋅ 𝑜 F ⁡ OrdIso E F supp ∅ ⁡ k + 𝑜 z ∅
10 1 2 3 8 4 9 cantnfval ⊢ φ → A CNF B ⁡ F = seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 OrdIso E F supp ∅ ⁡ k ⋅ 𝑜 F ⁡ OrdIso E F supp ∅ ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ OrdIso E F supp ∅
11 ovexd ⊢ φ → F supp ∅ ∈ V
12 8 oion ⊢ F supp ∅ ∈ V → dom ⁡ OrdIso E F supp ∅ ∈ On
13 sucidg ⊢ dom ⁡ OrdIso E F supp ∅ ∈ On → dom ⁡ OrdIso E F supp ∅ ∈ suc ⁡ dom ⁡ OrdIso E F supp ∅
14 11 12 13 3syl ⊢ φ → dom ⁡ OrdIso E F supp ∅ ∈ suc ⁡ dom ⁡ OrdIso E F supp ∅
15 1 2 3 8 4 cantnfcl ⊢ φ → E We supp ∅⁡ F ∧ dom ⁡ OrdIso E F supp ∅ ∈ ω
16 15 simpld ⊢ φ → E We supp ∅⁡ F
17 8 oiiso ⊢ F supp ∅ ∈ V ∧ E We supp ∅⁡ F → OrdIso E F supp ∅ Isom E , E dom ⁡ OrdIso E F supp ∅ F supp ∅
18 11 16 17 syl2anc ⊢ φ → OrdIso E F supp ∅ Isom E , E dom ⁡ OrdIso E F supp ∅ F supp ∅
19 isof1o ⊢ OrdIso E F supp ∅ Isom E , E dom ⁡ OrdIso E F supp ∅ F supp ∅ → OrdIso E F supp ∅ : dom ⁡ OrdIso E F supp ∅ ⟶ 1-1 onto F supp ∅
20 f1ofo ⊢ OrdIso E F supp ∅ : dom ⁡ OrdIso E F supp ∅ ⟶ 1-1 onto F supp ∅ → OrdIso E F supp ∅ : dom ⁡ OrdIso E F supp ∅ ⟶ onto F supp ∅
21 foima ⊢ OrdIso E F supp ∅ : dom ⁡ OrdIso E F supp ∅ ⟶ onto F supp ∅ → OrdIso E F supp ∅ dom ⁡ OrdIso E F supp ∅ = F supp ∅
22 18 19 20 21 4syl ⊢ φ → OrdIso E F supp ∅ dom ⁡ OrdIso E F supp ∅ = F supp ∅
23 22 7 eqsstrd ⊢ φ → OrdIso E F supp ∅ dom ⁡ OrdIso E F supp ∅ ⊆ C
24 1 2 3 8 4 9 5 14 6 23 cantnflt ⊢ φ → seq ω k ∈ V , z ∈ V ⟼ A ↑ 𝑜 OrdIso E F supp ∅ ⁡ k ⋅ 𝑜 F ⁡ OrdIso E F supp ∅ ⁡ k + 𝑜 z ∅ ⁡ dom ⁡ OrdIso E F supp ∅ ∈ A ↑ 𝑜 C
25 10 24 eqeltrd ⊢ φ → A CNF B ⁡ F ∈ A ↑ 𝑜 C