dnnumch1

Description: Define an enumeration of a set from a choice function; second part, it restricts to a bijection.EDITORIAL: overlaps dfac8a . (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	dnnumch1	$⊢ φ \to \exists x \in On ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A$

Proof

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		recsval	$⊢ x \in On \to recs ((z \in V ⟼ G (A ∖ ran z))) (x) = (z \in V ⟼ G (A ∖ ran z)) ({recs ((z \in V ⟼ G (A ∖ ran z))) ↾}_{x})$
5	1	fveq1i	$⊢ F (x) = recs ((z \in V ⟼ G (A ∖ ran z))) (x)$
6	1	tfr1	$⊢ F Fn On$
7		fnfun	$⊢ F Fn On \to Fun F$
8	6 7	ax-mp	$⊢ Fun F$
9		vex	$⊢ x \in V$
10		resfunexg	$⊢ (Fun F \land x \in V) \to {F ↾}_{x} \in V$
11	8 9 10	mp2an	$⊢ {F ↾}_{x} \in V$
12		rneq	$⊢ w = {F ↾}_{x} \to ran w = ran ({F ↾}_{x})$
13		df-ima	$⊢ F [x] = ran ({F ↾}_{x})$
14	12 13	eqtr4di	$⊢ w = {F ↾}_{x} \to ran w = F [x]$
15	14	difeq2d	$⊢ w = {F ↾}_{x} \to A ∖ ran w = A ∖ F [x]$
16	15	fveq2d	$⊢ w = {F ↾}_{x} \to G (A ∖ ran w) = G (A ∖ F [x])$
17		rneq	$⊢ z = w \to ran z = ran w$
18	17	difeq2d	$⊢ z = w \to A ∖ ran z = A ∖ ran w$
19	18	fveq2d	$⊢ z = w \to G (A ∖ ran z) = G (A ∖ ran w)$
20	19	cbvmptv	$⊢ (z \in V ⟼ G (A ∖ ran z)) = (w \in V ⟼ G (A ∖ ran w))$
21		fvex	$⊢ G (A ∖ F [x]) \in V$
22	16 20 21	fvmpt	$⊢ {F ↾}_{x} \in V \to (z \in V ⟼ G (A ∖ ran z)) ({F ↾}_{x}) = G (A ∖ F [x])$
23	11 22	ax-mp	$⊢ (z \in V ⟼ G (A ∖ ran z)) ({F ↾}_{x}) = G (A ∖ F [x])$
24	1	reseq1i	$⊢ {F ↾}_{x} = {recs ((z \in V ⟼ G (A ∖ ran z))) ↾}_{x}$
25	24	fveq2i	$⊢ (z \in V ⟼ G (A ∖ ran z)) ({F ↾}_{x}) = (z \in V ⟼ G (A ∖ ran z)) ({recs ((z \in V ⟼ G (A ∖ ran z))) ↾}_{x})$
26	23 25	eqtr3i	$⊢ G (A ∖ F [x]) = (z \in V ⟼ G (A ∖ ran z)) ({recs ((z \in V ⟼ G (A ∖ ran z))) ↾}_{x})$
27	4 5 26	3eqtr4g	$⊢ x \in On \to F (x) = G (A ∖ F [x])$
28	27	ad2antlr	$⊢ ((φ \land x \in On) \land A ∖ F [x] \neq \emptyset) \to F (x) = G (A ∖ F [x])$
29		difss	$⊢ A ∖ F [x] \subseteq A$
30		elpw2g	$⊢ A \in V \to (A ∖ F [x] \in 𝒫 A \leftrightarrow A ∖ F [x] \subseteq A)$
31	2 30	syl	$⊢ φ \to (A ∖ F [x] \in 𝒫 A \leftrightarrow A ∖ F [x] \subseteq A)$
32	29 31	mpbiri	$⊢ φ \to A ∖ F [x] \in 𝒫 A$
33		neeq1	$⊢ y = A ∖ F [x] \to (y \neq \emptyset \leftrightarrow A ∖ F [x] \neq \emptyset)$
34		fveq2	$⊢ y = A ∖ F [x] \to G (y) = G (A ∖ F [x])$
35		id	$⊢ y = A ∖ F [x] \to y = A ∖ F [x]$
36	34 35	eleq12d	$⊢ y = A ∖ F [x] \to (G (y) \in y \leftrightarrow G (A ∖ F [x]) \in (A ∖ F [x]))$
37	33 36	imbi12d	$⊢ y = A ∖ F [x] \to ((y \neq \emptyset \to G (y) \in y) \leftrightarrow (A ∖ F [x] \neq \emptyset \to G (A ∖ F [x]) \in (A ∖ F [x])))$
38	37	rspcva	$⊢ (A ∖ F [x] \in 𝒫 A \land \forall y \in 𝒫 A (y \neq \emptyset \to G (y) \in y)) \to (A ∖ F [x] \neq \emptyset \to G (A ∖ F [x]) \in (A ∖ F [x]))$
39	32 3 38	syl2anc	$⊢ φ \to (A ∖ F [x] \neq \emptyset \to G (A ∖ F [x]) \in (A ∖ F [x]))$
40	39	adantr	$⊢ (φ \land x \in On) \to (A ∖ F [x] \neq \emptyset \to G (A ∖ F [x]) \in (A ∖ F [x]))$
41	40	imp	$⊢ ((φ \land x \in On) \land A ∖ F [x] \neq \emptyset) \to G (A ∖ F [x]) \in (A ∖ F [x])$
42	28 41	eqeltrd	$⊢ ((φ \land x \in On) \land A ∖ F [x] \neq \emptyset) \to F (x) \in (A ∖ F [x])$
43	42	ex	$⊢ (φ \land x \in On) \to (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x]))$
44	43	ralrimiva	$⊢ φ \to \forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x]))$
45	6	tz7.49c	$⊢ (A \in V \land \forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x]))) \to \exists x \in On ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A$
46	2 44 45	syl2anc	$⊢ φ \to \exists x \in On ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A$

Metamath Proof Explorer

Theorem dnnumch1

Proof