acnrcl

Description: Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	acnrcl	$⊢ X \in \underline{AC} A \to A \in V$

Step	Hyp	Ref	Expression
1		ne0i	$⊢ X \in \{x \| (A \in V \land \forall f \in ({(𝒫 x ∖ \{\emptyset\})}^{A}) \exists g \forall y \in A g (y) \in f (y))\} \to \{x \| (A \in V \land \forall f \in ({(𝒫 x ∖ \{\emptyset\})}^{A}) \exists g \forall y \in A g (y) \in f (y))\} \neq \emptyset$
2		abn0	$⊢ \{x \| (A \in V \land \forall f \in ({(𝒫 x ∖ \{\emptyset\})}^{A}) \exists g \forall y \in A g (y) \in f (y))\} \neq \emptyset \leftrightarrow \exists x (A \in V \land \forall f \in ({(𝒫 x ∖ \{\emptyset\})}^{A}) \exists g \forall y \in A g (y) \in f (y))$
3		simpl	$⊢ (A \in V \land \forall f \in ({(𝒫 x ∖ \{\emptyset\})}^{A}) \exists g \forall y \in A g (y) \in f (y)) \to A \in V$
4	3	exlimiv	$⊢ \exists x (A \in V \land \forall f \in ({(𝒫 x ∖ \{\emptyset\})}^{A}) \exists g \forall y \in A g (y) \in f (y)) \to A \in V$
5	2 4	sylbi	$⊢ \{x \| (A \in V \land \forall f \in ({(𝒫 x ∖ \{\emptyset\})}^{A}) \exists g \forall y \in A g (y) \in f (y))\} \neq \emptyset \to A \in V$
6	1 5	syl	$⊢ X \in \{x \| (A \in V \land \forall f \in ({(𝒫 x ∖ \{\emptyset\})}^{A}) \exists g \forall y \in A g (y) \in f (y))\} \to A \in V$
7		df-acn	$⊢ \underline{AC} A = \{x \| (A \in V \land \forall f \in ({(𝒫 x ∖ \{\emptyset\})}^{A}) \exists g \forall y \in A g (y) \in f (y))\}$
8	6 7	eleq2s	$⊢ X \in \underline{AC} A \to A \in V$

Metamath Proof Explorer