dfac8alem

Description: Lemma for dfac8a . If the power set of a set has a choice function, then the set is numerable. (Contributed by NM, 10-Feb-1997) (Revised by Mario Carneiro, 5-Jan-2013)

	Ref	Expression
Hypotheses	dfac8alem.2	$⊢ F = recs (G)$
	dfac8alem.3	$⊢ G = (f \in V ⟼ g (A ∖ ran f))$
Assertion	dfac8alem	$⊢ A \in C \to (\exists g \forall y \in 𝒫 A (y \neq \emptyset \to g (y) \in y) \to A \in dom card)$

Proof

Step	Hyp	Ref	Expression
1		dfac8alem.2	$⊢ F = recs (G)$
2		dfac8alem.3	$⊢ G = (f \in V ⟼ g (A ∖ ran f))$
3		elex	$⊢ A \in C \to A \in V$
4		difss	$⊢ A ∖ F [x] \subseteq A$
5		elpw2g	$⊢ A \in V \to (A ∖ F [x] \in 𝒫 A \leftrightarrow A ∖ F [x] \subseteq A)$
6	4 5	mpbiri	$⊢ A \in V \to A ∖ F [x] \in 𝒫 A$
7		neeq1	$⊢ y = A ∖ F [x] \to (y \neq \emptyset \leftrightarrow A ∖ F [x] \neq \emptyset)$
8		fveq2	$⊢ y = A ∖ F [x] \to g (y) = g (A ∖ F [x])$
9		id	$⊢ y = A ∖ F [x] \to y = A ∖ F [x]$
10	8 9	eleq12d	$⊢ y = A ∖ F [x] \to (g (y) \in y \leftrightarrow g (A ∖ F [x]) \in (A ∖ F [x]))$
11	7 10	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])))$
12	11	rspcv	$⊢ A ∖ F [x] \in 𝒫 A \to (\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])))$
13	6 12	syl	$⊢ A \in V \to (\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])))$
14	13	3imp	$⊢ (A \in V \land \forall y \in 𝒫 A (y \neq \emptyset \to g (y) \in y) \land A ∖ F [x] \neq \emptyset) \to g (A ∖ F [x]) \in (A ∖ F [x])$
15	1	tfr2	$⊢ x \in On \to F (x) = G ({F ↾}_{x})$
16	1	tfr1	$⊢ F Fn On$
17		fnfun	$⊢ F Fn On \to Fun F$
18	16 17	ax-mp	$⊢ Fun F$
19		vex	$⊢ x \in V$
20		resfunexg	$⊢ (Fun F \land x \in V) \to {F ↾}_{x} \in V$
21	18 19 20	mp2an	$⊢ {F ↾}_{x} \in V$
22		rneq	$⊢ f = {F ↾}_{x} \to ran f = ran ({F ↾}_{x})$
23		df-ima	$⊢ F [x] = ran ({F ↾}_{x})$
24	22 23	eqtr4di	$⊢ f = {F ↾}_{x} \to ran f = F [x]$
25	24	difeq2d	$⊢ f = {F ↾}_{x} \to A ∖ ran f = A ∖ F [x]$
26	25	fveq2d	$⊢ f = {F ↾}_{x} \to g (A ∖ ran f) = g (A ∖ F [x])$
27		fvex	$⊢ g (A ∖ F [x]) \in V$
28	26 2 27	fvmpt	$⊢ {F ↾}_{x} \in V \to G ({F ↾}_{x}) = g (A ∖ F [x])$
29	21 28	ax-mp	$⊢ G ({F ↾}_{x}) = g (A ∖ F [x])$
30	15 29	eqtrdi	$⊢ x \in On \to F (x) = g (A ∖ F [x])$
31	30	eleq1d	$⊢ x \in On \to (F (x) \in (A ∖ F [x]) \leftrightarrow g (A ∖ F [x]) \in (A ∖ F [x]))$
32	14 31	syl5ibrcom	$⊢ (A \in V \land \forall y \in 𝒫 A (y \neq \emptyset \to g (y) \in y) \land A ∖ F [x] \neq \emptyset) \to (x \in On \to F (x) \in (A ∖ F [x]))$
33	32	3expia	$⊢ (A \in V \land \forall y \in 𝒫 A (y \neq \emptyset \to g (y) \in y)) \to (A ∖ F [x] \neq \emptyset \to (x \in On \to F (x) \in (A ∖ F [x])))$
34	33	com23	$⊢ (A \in V \land \forall y \in 𝒫 A (y \neq \emptyset \to g (y) \in y)) \to (x \in On \to (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x])))$
35	34	ralrimiv	$⊢ (A \in V \land \forall y \in 𝒫 A (y \neq \emptyset \to g (y) \in y)) \to \forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x]))$
36	35	ex	$⊢ A \in V \to (\forall y \in 𝒫 A (y \neq \emptyset \to g (y) \in y) \to \forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x])))$
37	16	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$
38	37	ex	$⊢ A \in V \to (\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)$
39	19	f1oen	$⊢ ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A \to x \approx A$
40		isnumi	$⊢ (x \in On \land x \approx A) \to A \in dom card$
41	39 40	sylan2	$⊢ (x \in On \land ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A) \to A \in dom card$
42	41	rexlimiva	$⊢ \exists x \in On ({F ↾}_{x}) : x \underset{1-1 onto}{⟶} A \to A \in dom card$
43	38 42	syl6	$⊢ A \in V \to (\forall x \in On (A ∖ F [x] \neq \emptyset \to F (x) \in (A ∖ F [x])) \to A \in dom card)$
44	36 43	syld	$⊢ A \in V \to (\forall y \in 𝒫 A (y \neq \emptyset \to g (y) \in y) \to A \in dom card)$
45	3 44	syl	$⊢ A \in C \to (\forall y \in 𝒫 A (y \neq \emptyset \to g (y) \in y) \to A \in dom card)$
46	45	exlimdv	$⊢ A \in C \to (\exists g \forall y \in 𝒫 A (y \neq \emptyset \to g (y) \in y) \to A \in dom card)$

Metamath Proof Explorer

Theorem dfac8alem

Proof