ac5num

Description: A version of ac5b with the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015)

		Ref	Expression
	Assertion	ac5num	$⊢ (⋃ A \in dom card \land \neg \emptyset \in A) \to \exists f (f : A ⟶ ⋃ A \land \forall x \in A f (x) \in x)$

Proof

Step	Hyp	Ref	Expression
1		uniexr	$⊢ ⋃ A \in dom card \to A \in V$
2		dfac8b	$⊢ ⋃ A \in dom card \to \exists r r We ⋃ A$
3		dfac8c	$⊢ A \in V \to (\exists r r We ⋃ A \to \exists g \forall x \in A (x \neq \emptyset \to g (x) \in x))$
4	1 2 3	sylc	$⊢ ⋃ A \in dom card \to \exists g \forall x \in A (x \neq \emptyset \to g (x) \in x)$
5	4	adantr	$⊢ (⋃ A \in dom card \land \neg \emptyset \in A) \to \exists g \forall x \in A (x \neq \emptyset \to g (x) \in x)$
6	1	ad2antrr	$⊢ ((⋃ A \in dom card \land \neg \emptyset \in A) \land \forall x \in A (x \neq \emptyset \to g (x) \in x)) \to A \in V$
7	6	mptexd	$⊢ ((⋃ A \in dom card \land \neg \emptyset \in A) \land \forall x \in A (x \neq \emptyset \to g (x) \in x)) \to (y \in A ⟼ g (y)) \in V$
8		nelne2	$⊢ (x \in A \land \neg \emptyset \in A) \to x \neq \emptyset$
9	8	ancoms	$⊢ (\neg \emptyset \in A \land x \in A) \to x \neq \emptyset$
10	9	adantll	$⊢ ((⋃ A \in dom card \land \neg \emptyset \in A) \land x \in A) \to x \neq \emptyset$
11		pm2.27	$⊢ x \neq \emptyset \to ((x \neq \emptyset \to g (x) \in x) \to g (x) \in x)$
12	10 11	syl	$⊢ ((⋃ A \in dom card \land \neg \emptyset \in A) \land x \in A) \to ((x \neq \emptyset \to g (x) \in x) \to g (x) \in x)$
13	12	ralimdva	$⊢ (⋃ A \in dom card \land \neg \emptyset \in A) \to (\forall x \in A (x \neq \emptyset \to g (x) \in x) \to \forall x \in A g (x) \in x)$
14	13	imp	$⊢ ((⋃ A \in dom card \land \neg \emptyset \in A) \land \forall x \in A (x \neq \emptyset \to g (x) \in x)) \to \forall x \in A g (x) \in x$
15		fveq2	$⊢ x = y \to g (x) = g (y)$
16		id	$⊢ x = y \to x = y$
17	15 16	eleq12d	$⊢ x = y \to (g (x) \in x \leftrightarrow g (y) \in y)$
18	17	rspccva	$⊢ (\forall x \in A g (x) \in x \land y \in A) \to g (y) \in y$
19	14 18	sylan	$⊢ (((⋃ A \in dom card \land \neg \emptyset \in A) \land \forall x \in A (x \neq \emptyset \to g (x) \in x)) \land y \in A) \to g (y) \in y$
20		elunii	$⊢ (g (y) \in y \land y \in A) \to g (y) \in ⋃ A$
21	19 20	sylancom	$⊢ (((⋃ A \in dom card \land \neg \emptyset \in A) \land \forall x \in A (x \neq \emptyset \to g (x) \in x)) \land y \in A) \to g (y) \in ⋃ A$
22	21	fmpttd	$⊢ ((⋃ A \in dom card \land \neg \emptyset \in A) \land \forall x \in A (x \neq \emptyset \to g (x) \in x)) \to (y \in A ⟼ g (y)) : A ⟶ ⋃ A$
23		fveq2	$⊢ y = x \to g (y) = g (x)$
24		eqid	$⊢ (y \in A ⟼ g (y)) = (y \in A ⟼ g (y))$
25		fvex	$⊢ g (x) \in V$
26	23 24 25	fvmpt	$⊢ x \in A \to (y \in A ⟼ g (y)) (x) = g (x)$
27	26	eleq1d	$⊢ x \in A \to ((y \in A ⟼ g (y)) (x) \in x \leftrightarrow g (x) \in x)$
28	27	ralbiia	$⊢ \forall x \in A (y \in A ⟼ g (y)) (x) \in x \leftrightarrow \forall x \in A g (x) \in x$
29	14 28	sylibr	$⊢ ((⋃ A \in dom card \land \neg \emptyset \in A) \land \forall x \in A (x \neq \emptyset \to g (x) \in x)) \to \forall x \in A (y \in A ⟼ g (y)) (x) \in x$
30	22 29	jca	$⊢ ((⋃ A \in dom card \land \neg \emptyset \in A) \land \forall x \in A (x \neq \emptyset \to g (x) \in x)) \to ((y \in A ⟼ g (y)) : A ⟶ ⋃ A \land \forall x \in A (y \in A ⟼ g (y)) (x) \in x)$
31		feq1	$⊢ f = (y \in A ⟼ g (y)) \to (f : A ⟶ ⋃ A \leftrightarrow (y \in A ⟼ g (y)) : A ⟶ ⋃ A)$
32		fveq1	$⊢ f = (y \in A ⟼ g (y)) \to f (x) = (y \in A ⟼ g (y)) (x)$
33	32	eleq1d	$⊢ f = (y \in A ⟼ g (y)) \to (f (x) \in x \leftrightarrow (y \in A ⟼ g (y)) (x) \in x)$
34	33	ralbidv	$⊢ f = (y \in A ⟼ g (y)) \to (\forall x \in A f (x) \in x \leftrightarrow \forall x \in A (y \in A ⟼ g (y)) (x) \in x)$
35	31 34	anbi12d	$⊢ f = (y \in A ⟼ g (y)) \to ((f : A ⟶ ⋃ A \land \forall x \in A f (x) \in x) \leftrightarrow ((y \in A ⟼ g (y)) : A ⟶ ⋃ A \land \forall x \in A (y \in A ⟼ g (y)) (x) \in x))$
36	7 30 35	spcedv	$⊢ ((⋃ A \in dom card \land \neg \emptyset \in A) \land \forall x \in A (x \neq \emptyset \to g (x) \in x)) \to \exists f (f : A ⟶ ⋃ A \land \forall x \in A f (x) \in x)$
37	5 36	exlimddv	$⊢ (⋃ A \in dom card \land \neg \emptyset \in A) \to \exists f (f : A ⟶ ⋃ A \land \forall x \in A f (x) \in x)$

Metamath Proof Explorer

Theorem ac5num

Proof