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 ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
cantnflt2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
cantnflt2.a ⊢ ( 𝜑 → ∅ ∈ 𝐴 )
cantnflt2.c ⊢ ( 𝜑 → 𝐶 ∈ On )
cantnflt2.s ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ 𝐶 )
Assertion cantnflt2 ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( 𝐴 ↑o 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s ⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2 cantnfs.a ⊢ ( 𝜑 → 𝐴 ∈ On )
3 cantnfs.b ⊢ ( 𝜑 → 𝐵 ∈ On )
4 cantnflt2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑆 )
5 cantnflt2.a ⊢ ( 𝜑 → ∅ ∈ 𝐴 )
6 cantnflt2.c ⊢ ( 𝜑 → 𝐶 ∈ On )
7 cantnflt2.s ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ 𝐶 )
8 eqid ⊢ OrdIso ( E , ( 𝐹 supp ∅ ) ) = OrdIso ( E , ( 𝐹 supp ∅ ) )
9 eqid ⊢ seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝐹 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( OrdIso ( E , ( 𝐹 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) = seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝐹 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( OrdIso ( E , ( 𝐹 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ )
10 1 2 3 8 4 9 cantnfval ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) = ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝐹 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( OrdIso ( E , ( 𝐹 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ( 𝐹 supp ∅ ) ) ) )
11 ovexd ⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ∈ V )
12 8 oion ⊢ ( ( 𝐹 supp ∅ ) ∈ V → dom OrdIso ( E , ( 𝐹 supp ∅ ) ) ∈ On )
13 sucidg ⊢ ( dom OrdIso ( E , ( 𝐹 supp ∅ ) ) ∈ On → dom OrdIso ( E , ( 𝐹 supp ∅ ) ) ∈ suc dom OrdIso ( E , ( 𝐹 supp ∅ ) ) )
14 11 12 13 3syl ⊢ ( 𝜑 → dom OrdIso ( E , ( 𝐹 supp ∅ ) ) ∈ suc dom OrdIso ( E , ( 𝐹 supp ∅ ) ) )
15 1 2 3 8 4 cantnfcl ⊢ ( 𝜑 → ( E We ( 𝐹 supp ∅ ) ∧ dom OrdIso ( E , ( 𝐹 supp ∅ ) ) ∈ ω ) )
16 15 simpld ⊢ ( 𝜑 → E We ( 𝐹 supp ∅ ) )
17 8 oiiso ⊢ ( ( ( 𝐹 supp ∅ ) ∈ V ∧ E We ( 𝐹 supp ∅ ) ) → OrdIso ( E , ( 𝐹 supp ∅ ) ) Isom E , E ( dom OrdIso ( E , ( 𝐹 supp ∅ ) ) , ( 𝐹 supp ∅ ) ) )
18 11 16 17 syl2anc ⊢ ( 𝜑 → OrdIso ( E , ( 𝐹 supp ∅ ) ) Isom E , E ( dom OrdIso ( E , ( 𝐹 supp ∅ ) ) , ( 𝐹 supp ∅ ) ) )
19 isof1o ⊢ ( OrdIso ( E , ( 𝐹 supp ∅ ) ) Isom E , E ( dom OrdIso ( E , ( 𝐹 supp ∅ ) ) , ( 𝐹 supp ∅ ) ) → OrdIso ( E , ( 𝐹 supp ∅ ) ) : dom OrdIso ( E , ( 𝐹 supp ∅ ) ) –1-1-onto→ ( 𝐹 supp ∅ ) )
20 f1ofo ⊢ ( OrdIso ( E , ( 𝐹 supp ∅ ) ) : dom OrdIso ( E , ( 𝐹 supp ∅ ) ) –1-1-onto→ ( 𝐹 supp ∅ ) → OrdIso ( E , ( 𝐹 supp ∅ ) ) : dom OrdIso ( E , ( 𝐹 supp ∅ ) ) –onto→ ( 𝐹 supp ∅ ) )
21 foima ⊢ ( OrdIso ( E , ( 𝐹 supp ∅ ) ) : dom OrdIso ( E , ( 𝐹 supp ∅ ) ) –onto→ ( 𝐹 supp ∅ ) → ( OrdIso ( E , ( 𝐹 supp ∅ ) ) “ dom OrdIso ( E , ( 𝐹 supp ∅ ) ) ) = ( 𝐹 supp ∅ ) )
22 18 19 20 21 4syl ⊢ ( 𝜑 → ( OrdIso ( E , ( 𝐹 supp ∅ ) ) “ dom OrdIso ( E , ( 𝐹 supp ∅ ) ) ) = ( 𝐹 supp ∅ ) )
23 22 7 eqsstrd ⊢ ( 𝜑 → ( OrdIso ( E , ( 𝐹 supp ∅ ) ) “ dom OrdIso ( E , ( 𝐹 supp ∅ ) ) ) ⊆ 𝐶 )
24 1 2 3 8 4 9 5 14 6 23 cantnflt ⊢ ( 𝜑 → ( seqω ( ( 𝑘 ∈ V , 𝑧 ∈ V ↦ ( ( ( 𝐴 ↑o ( OrdIso ( E , ( 𝐹 supp ∅ ) ) ‘ 𝑘 ) ) ·o ( 𝐹 ‘ ( OrdIso ( E , ( 𝐹 supp ∅ ) ) ‘ 𝑘 ) ) ) +o 𝑧 ) ) , ∅ ) ‘ dom OrdIso ( E , ( 𝐹 supp ∅ ) ) ) ∈ ( 𝐴 ↑o 𝐶 ) )
25 10 24 eqeltrd ⊢ ( 𝜑 → ( ( 𝐴 CNF 𝐵 ) ‘ 𝐹 ) ∈ ( 𝐴 ↑o 𝐶 ) )