dfac8clem

		Ref	Expression
	Hypothesis	dfac8clem.1	$⊢ F = (s \in (A ∖ \{\emptyset\}) ⟼ (ι a \in s \| \forall b \in s \neg b r a))$
	Assertion	dfac8clem	$⊢ A \in B \to (\exists r r We ⋃ A \to \exists f \forall z \in A (z \neq \emptyset \to f (z) \in z))$

Proof

Step	Hyp	Ref	Expression
1		dfac8clem.1	$⊢ F = (s \in (A ∖ \{\emptyset\}) ⟼ (ι a \in s \| \forall b \in s \neg b r a))$
2		eldifsn	$⊢ s \in (A ∖ \{\emptyset\}) \leftrightarrow (s \in A \land s \neq \emptyset)$
3		elssuni	$⊢ s \in A \to s \subseteq ⋃ A$
4	3	ad2antrl	$⊢ ((A \in B \land r We ⋃ A) \land (s \in A \land s \neq \emptyset)) \to s \subseteq ⋃ A$
5		simplr	$⊢ ((A \in B \land r We ⋃ A) \land (s \in A \land s \neq \emptyset)) \to r We ⋃ A$
6		vex	$⊢ r \in V$
7		exse2	$⊢ r \in V \to r Se ⋃ A$
8	6 7	mp1i	$⊢ ((A \in B \land r We ⋃ A) \land (s \in A \land s \neq \emptyset)) \to r Se ⋃ A$
9		simprr	$⊢ ((A \in B \land r We ⋃ A) \land (s \in A \land s \neq \emptyset)) \to s \neq \emptyset$
10		wereu2	$⊢ ((r We ⋃ A \land r Se ⋃ A) \land (s \subseteq ⋃ A \land s \neq \emptyset)) \to \exists! a \in s \forall b \in s \neg b r a$
11	5 8 4 9 10	syl22anc	$⊢ ((A \in B \land r We ⋃ A) \land (s \in A \land s \neq \emptyset)) \to \exists! a \in s \forall b \in s \neg b r a$
12		riotacl	$⊢ \exists! a \in s \forall b \in s \neg b r a \to (ι a \in s \| \forall b \in s \neg b r a) \in s$
13	11 12	syl	$⊢ ((A \in B \land r We ⋃ A) \land (s \in A \land s \neq \emptyset)) \to (ι a \in s \| \forall b \in s \neg b r a) \in s$
14	4 13	sseldd	$⊢ ((A \in B \land r We ⋃ A) \land (s \in A \land s \neq \emptyset)) \to (ι a \in s \| \forall b \in s \neg b r a) \in ⋃ A$
15	2 14	sylan2b	$⊢ ((A \in B \land r We ⋃ A) \land s \in (A ∖ \{\emptyset\})) \to (ι a \in s \| \forall b \in s \neg b r a) \in ⋃ A$
16	15 1	fmptd	$⊢ (A \in B \land r We ⋃ A) \to F : A ∖ \{\emptyset\} ⟶ ⋃ A$
17		difexg	$⊢ A \in B \to A ∖ \{\emptyset\} \in V$
18	17	adantr	$⊢ (A \in B \land r We ⋃ A) \to A ∖ \{\emptyset\} \in V$
19		uniexg	$⊢ A \in B \to ⋃ A \in V$
20	19	adantr	$⊢ (A \in B \land r We ⋃ A) \to ⋃ A \in V$
21		fex2	$⊢ (F : A ∖ \{\emptyset\} ⟶ ⋃ A \land A ∖ \{\emptyset\} \in V \land ⋃ A \in V) \to F \in V$
22	16 18 20 21	syl3anc	$⊢ (A \in B \land r We ⋃ A) \to F \in V$
23		riotaex	$⊢ (ι a \in s \| \forall b \in s \neg b r a) \in V$
24	1	fvmpt2	$⊢ (s \in (A ∖ \{\emptyset\}) \land (ι a \in s \| \forall b \in s \neg b r a) \in V) \to F (s) = (ι a \in s \| \forall b \in s \neg b r a)$
25	23 24	mpan2	$⊢ s \in (A ∖ \{\emptyset\}) \to F (s) = (ι a \in s \| \forall b \in s \neg b r a)$
26	2 25	sylbir	$⊢ (s \in A \land s \neq \emptyset) \to F (s) = (ι a \in s \| \forall b \in s \neg b r a)$
27	26	adantl	$⊢ ((A \in B \land r We ⋃ A) \land (s \in A \land s \neq \emptyset)) \to F (s) = (ι a \in s \| \forall b \in s \neg b r a)$
28	27 13	eqeltrd	$⊢ ((A \in B \land r We ⋃ A) \land (s \in A \land s \neq \emptyset)) \to F (s) \in s$
29	28	expr	$⊢ ((A \in B \land r We ⋃ A) \land s \in A) \to (s \neq \emptyset \to F (s) \in s)$
30	29	ralrimiva	$⊢ (A \in B \land r We ⋃ A) \to \forall s \in A (s \neq \emptyset \to F (s) \in s)$
31		nfv	$⊢ Ⅎ s z \neq \emptyset$
32		nfmpt1	$⊢ \underline{Ⅎ} s (s \in (A ∖ \{\emptyset\}) ⟼ (ι a \in s \| \forall b \in s \neg b r a))$
33	1 32	nfcxfr	$⊢ \underline{Ⅎ} s F$
34		nfcv	$⊢ \underline{Ⅎ} s z$
35	33 34	nffv	$⊢ \underline{Ⅎ} s F (z)$
36	35	nfel1	$⊢ Ⅎ s F (z) \in z$
37	31 36	nfim	$⊢ Ⅎ s (z \neq \emptyset \to F (z) \in z)$
38		nfv	$⊢ Ⅎ z (s \neq \emptyset \to F (s) \in s)$
39		neeq1	$⊢ z = s \to (z \neq \emptyset \leftrightarrow s \neq \emptyset)$
40		fveq2	$⊢ z = s \to F (z) = F (s)$
41		id	$⊢ z = s \to z = s$
42	40 41	eleq12d	$⊢ z = s \to (F (z) \in z \leftrightarrow F (s) \in s)$
43	39 42	imbi12d	$⊢ z = s \to ((z \neq \emptyset \to F (z) \in z) \leftrightarrow (s \neq \emptyset \to F (s) \in s))$
44	37 38 43	cbvralw	$⊢ \forall z \in A (z \neq \emptyset \to F (z) \in z) \leftrightarrow \forall s \in A (s \neq \emptyset \to F (s) \in s)$
45	30 44	sylibr	$⊢ (A \in B \land r We ⋃ A) \to \forall z \in A (z \neq \emptyset \to F (z) \in z)$
46		fveq1	$⊢ f = F \to f (z) = F (z)$
47	46	eleq1d	$⊢ f = F \to (f (z) \in z \leftrightarrow F (z) \in z)$
48	47	imbi2d	$⊢ f = F \to ((z \neq \emptyset \to f (z) \in z) \leftrightarrow (z \neq \emptyset \to F (z) \in z))$
49	48	ralbidv	$⊢ f = F \to (\forall z \in A (z \neq \emptyset \to f (z) \in z) \leftrightarrow \forall z \in A (z \neq \emptyset \to F (z) \in z))$
50	22 45 49	spcedv	$⊢ (A \in B \land r We ⋃ A) \to \exists f \forall z \in A (z \neq \emptyset \to f (z) \in z)$
51	50	ex	$⊢ A \in B \to (r We ⋃ A \to \exists f \forall z \in A (z \neq \emptyset \to f (z) \in z))$
52	51	exlimdv	$⊢ A \in B \to (\exists r r We ⋃ A \to \exists f \forall z \in A (z \neq \emptyset \to f (z) \in z))$

Metamath Proof Explorer

Theorem dfac8clem

Proof