Theorem cfsmo

Description: The map in cff1 can be assumed to be a strictly monotone ordinal function without loss of generality. (Contributed by Mario Carneiro, 28-Feb-2013)

	Ref	Expression
Assertion	cfsmo	⊢ ( 𝐴 ∈ On → ∃ 𝑓 ( 𝑓 : ( cf ‘ 𝐴 ) ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dmeq	⊢ ( 𝑥 = 𝑧 → dom 𝑥 = dom 𝑧 )
2	1	fveq2d	⊢ ( 𝑥 = 𝑧 → ( ℎ ‘ dom 𝑥 ) = ( ℎ ‘ dom 𝑧 ) )
3		fveq2	⊢ ( 𝑛 = 𝑚 → ( 𝑥 ‘ 𝑛 ) = ( 𝑥 ‘ 𝑚 ) )
4		suceq	⊢ ( ( 𝑥 ‘ 𝑛 ) = ( 𝑥 ‘ 𝑚 ) → suc ( 𝑥 ‘ 𝑛 ) = suc ( 𝑥 ‘ 𝑚 ) )
5	3 4	syl	⊢ ( 𝑛 = 𝑚 → suc ( 𝑥 ‘ 𝑛 ) = suc ( 𝑥 ‘ 𝑚 ) )
6	5	cbviunv	⊢ ∪ 𝑛 ∈ dom 𝑥 suc ( 𝑥 ‘ 𝑛 ) = ∪ 𝑚 ∈ dom 𝑥 suc ( 𝑥 ‘ 𝑚 )
7		fveq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ‘ 𝑚 ) = ( 𝑧 ‘ 𝑚 ) )
8		suceq	⊢ ( ( 𝑥 ‘ 𝑚 ) = ( 𝑧 ‘ 𝑚 ) → suc ( 𝑥 ‘ 𝑚 ) = suc ( 𝑧 ‘ 𝑚 ) )
9	7 8	syl	⊢ ( 𝑥 = 𝑧 → suc ( 𝑥 ‘ 𝑚 ) = suc ( 𝑧 ‘ 𝑚 ) )
10	1 9	iuneq12d	⊢ ( 𝑥 = 𝑧 → ∪ 𝑚 ∈ dom 𝑥 suc ( 𝑥 ‘ 𝑚 ) = ∪ 𝑚 ∈ dom 𝑧 suc ( 𝑧 ‘ 𝑚 ) )
11	6 10	eqtrid	⊢ ( 𝑥 = 𝑧 → ∪ 𝑛 ∈ dom 𝑥 suc ( 𝑥 ‘ 𝑛 ) = ∪ 𝑚 ∈ dom 𝑧 suc ( 𝑧 ‘ 𝑚 ) )
12	2 11	uneq12d	⊢ ( 𝑥 = 𝑧 → ( ( ℎ ‘ dom 𝑥 ) ∪ ∪ 𝑛 ∈ dom 𝑥 suc ( 𝑥 ‘ 𝑛 ) ) = ( ( ℎ ‘ dom 𝑧 ) ∪ ∪ 𝑚 ∈ dom 𝑧 suc ( 𝑧 ‘ 𝑚 ) ) )
13	12	cbvmptv	⊢ ( 𝑥 ∈ V ↦ ( ( ℎ ‘ dom 𝑥 ) ∪ ∪ 𝑛 ∈ dom 𝑥 suc ( 𝑥 ‘ 𝑛 ) ) ) = ( 𝑧 ∈ V ↦ ( ( ℎ ‘ dom 𝑧 ) ∪ ∪ 𝑚 ∈ dom 𝑧 suc ( 𝑧 ‘ 𝑚 ) ) )
14		eqid	⊢ ( recs ( ( 𝑥 ∈ V ↦ ( ( ℎ ‘ dom 𝑥 ) ∪ ∪ 𝑛 ∈ dom 𝑥 suc ( 𝑥 ‘ 𝑛 ) ) ) ) ↾ ( cf ‘ 𝐴 ) ) = ( recs ( ( 𝑥 ∈ V ↦ ( ( ℎ ‘ dom 𝑥 ) ∪ ∪ 𝑛 ∈ dom 𝑥 suc ( 𝑥 ‘ 𝑛 ) ) ) ) ↾ ( cf ‘ 𝐴 ) )
15	13 14	cfsmolem	⊢ ( 𝐴 ∈ On → ∃ 𝑓 ( 𝑓 : ( cf ‘ 𝐴 ) ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ( cf ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )