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 ⊢ A ∈ On → ∃ f f : cf ⁡ A ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ f ⁡ w

Proof

Step Hyp Ref Expression
1 dmeq ⊢ x = z → dom ⁡ x = dom ⁡ z
2 1 fveq2d ⊢ x = z → h ⁡ dom ⁡ x = h ⁡ dom ⁡ z
3 fveq2 ⊢ n = m → x ⁡ n = x ⁡ m
4 suceq ⊢ x ⁡ n = x ⁡ m → suc ⁡ x ⁡ n = suc ⁡ x ⁡ m
5 3 4 syl ⊢ n = m → suc ⁡ x ⁡ n = suc ⁡ x ⁡ m
6 5 cbviunv ⊢ ⋃ n ∈ dom ⁡ x suc ⁡ x ⁡ n = ⋃ m ∈ dom ⁡ x suc ⁡ x ⁡ m
7 fveq1 ⊢ x = z → x ⁡ m = z ⁡ m
8 suceq ⊢ x ⁡ m = z ⁡ m → suc ⁡ x ⁡ m = suc ⁡ z ⁡ m
9 7 8 syl ⊢ x = z → suc ⁡ x ⁡ m = suc ⁡ z ⁡ m
10 1 9 iuneq12d ⊢ x = z → ⋃ m ∈ dom ⁡ x suc ⁡ x ⁡ m = ⋃ m ∈ dom ⁡ z suc ⁡ z ⁡ m
11 6 10 eqtrid ⊢ x = z → ⋃ n ∈ dom ⁡ x suc ⁡ x ⁡ n = ⋃ m ∈ dom ⁡ z suc ⁡ z ⁡ m
12 2 11 uneq12d ⊢ x = z → h ⁡ dom ⁡ x ∪ ⋃ n ∈ dom ⁡ x suc ⁡ x ⁡ n = h ⁡ dom ⁡ z ∪ ⋃ m ∈ dom ⁡ z suc ⁡ z ⁡ m
13 12 cbvmptv ⊢ x ∈ V ⟼ h ⁡ dom ⁡ x ∪ ⋃ n ∈ dom ⁡ x suc ⁡ x ⁡ n = z ∈ V ⟼ h ⁡ dom ⁡ z ∪ ⋃ m ∈ dom ⁡ z suc ⁡ z ⁡ m
14 eqid ⊢ recs ⁡ x ∈ V ⟼ h ⁡ dom ⁡ x ∪ ⋃ n ∈ dom ⁡ x suc ⁡ x ⁡ n ↾ cf ⁡ A = recs ⁡ x ∈ V ⟼ h ⁡ dom ⁡ x ∪ ⋃ n ∈ dom ⁡ x suc ⁡ x ⁡ n ↾ cf ⁡ A
15 13 14 cfsmolem ⊢ A ∈ On → ∃ f f : cf ⁡ A ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ cf ⁡ A z ⊆ f ⁡ w