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 \in On \to \exists f (f : cf (A) ⟶ A \land Smo f \land \forall z \in A \exists w \in cf (A) z \subseteq f (w))$

Proof

Step	Hyp	Ref	Expression
1		dmeq	$⊢ x = z \to dom x = dom z$
2	1	fveq2d	$⊢ x = z \to h (dom x) = h (dom z)$
3		fveq2	$⊢ n = m \to x (n) = x (m)$
4		suceq	$⊢ x (n) = x (m) \to suc x (n) = suc x (m)$
5	3 4	syl	$⊢ n = m \to suc x (n) = suc x (m)$
6	5	cbviunv	$⊢ ⋃_{n \in dom x} suc x (n) = ⋃_{m \in dom x} suc x (m)$
7		fveq1	$⊢ x = z \to x (m) = z (m)$
8		suceq	$⊢ x (m) = z (m) \to suc x (m) = suc z (m)$
9	7 8	syl	$⊢ x = z \to suc x (m) = suc z (m)$
10	1 9	iuneq12d	$⊢ x = z \to ⋃_{m \in dom x} suc x (m) = ⋃_{m \in dom z} suc z (m)$
11	6 10	eqtrid	$⊢ x = z \to ⋃_{n \in dom x} suc x (n) = ⋃_{m \in dom z} suc z (m)$
12	2 11	uneq12d	$⊢ x = z \to h (dom x) \cup ⋃_{n \in dom x} suc x (n) = h (dom z) \cup ⋃_{m \in dom z} suc z (m)$
13	12	cbvmptv	$⊢ (x \in V ⟼ h (dom x) \cup ⋃_{n \in dom x} suc x (n)) = (z \in V ⟼ h (dom z) \cup ⋃_{m \in dom z} suc z (m))$
14		eqid	$⊢ {recs ((x \in V ⟼ h (dom x) \cup ⋃_{n \in dom x} suc x (n))) ↾}_{cf (A)} = {recs ((x \in V ⟼ h (dom x) \cup ⋃_{n \in dom x} suc x (n))) ↾}_{cf (A)}$
15	13 14	cfsmolem	$⊢ A \in On \to \exists f (f : cf (A) ⟶ A \land Smo f \land \forall z \in A \exists w \in cf (A) z \subseteq f (w))$