This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐴 ) 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )