dnnumch2

Description: Define an enumeration (weak dominance version) of a set from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Hypotheses	dnnumch.f	$⊢ F = recs ((z \in V ⟼ G (A ∖ ran z)))$
	dnnumch.a	$⊢ φ \to A \in V$
	dnnumch.g	$⊢ φ \to \forall y \in 𝒫 A (y \neq \emptyset \to G (y) \in y)$
Assertion	dnnumch2	$⊢ φ \to A \subseteq ran F$

Step	Hyp	Ref	Expression
1		dnnumch.f	$⊢ F = recs ((z \in V ⟼ G (A ∖ ran z)))$
2		dnnumch.a	$⊢ φ \to A \in V$
3		dnnumch.g	$⊢ φ \to \forall y \in 𝒫 A (y \neq \emptyset \to G (y) \in y)$
4	1 2 3	dnnumch1	$⊢ φ \to \exists x \in On ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A$
5		f1ofo	$⊢ ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A \to ({F ↾}_{x}) : x \underset{onto}{⟶} A$
6		forn	$⊢ ({F ↾}_{x}) : x \underset{onto}{⟶} A \to ran ({F ↾}_{x}) = A$
7	5 6	syl	$⊢ ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A \to ran ({F ↾}_{x}) = A$
8		resss	$⊢ {F ↾}_{x} \subseteq F$
9		rnss	$⊢ {F ↾}_{x} \subseteq F \to ran ({F ↾}_{x}) \subseteq ran F$
10	8 9	mp1i	$⊢ ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A \to ran ({F ↾}_{x}) \subseteq ran F$
11	7 10	eqsstrrd	$⊢ ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A \to A \subseteq ran F$
12	11	a1i	$⊢ φ \to (({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A \to A \subseteq ran F)$
13	12	rexlimdvw	$⊢ φ \to (\exists x \in On ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A \to A \subseteq ran F)$
14	4 13	mpd	$⊢ φ \to A \subseteq ran F$

Metamath Proof Explorer