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 𝐶 ) )

Metamath Proof Explorer

Theorem cantnflt2

Proof