acni3

Description: The property of being a choice set of length A . (Contributed by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Hypothesis	acni3.1	$⊢ y = g (x) \to (φ \leftrightarrow ψ)$
	Assertion	acni3	$⊢ (X \in \underline{AC} A \land \forall x \in A \exists y \in X φ) \to \exists g (g : A ⟶ X \land \forall x \in A ψ)$

Step	Hyp	Ref	Expression
1		acni3.1	$⊢ y = g (x) \to (φ \leftrightarrow ψ)$
2		rabn0	$⊢ \{y \in X \| φ\} \neq \emptyset \leftrightarrow \exists y \in X φ$
3	2	biimpri	$⊢ \exists y \in X φ \to \{y \in X \| φ\} \neq \emptyset$
4		ssrab2	$⊢ \{y \in X \| φ\} \subseteq X$
5	3 4	jctil	$⊢ \exists y \in X φ \to (\{y \in X \| φ\} \subseteq X \land \{y \in X \| φ\} \neq \emptyset)$
6	5	ralimi	$⊢ \forall x \in A \exists y \in X φ \to \forall x \in A (\{y \in X \| φ\} \subseteq X \land \{y \in X \| φ\} \neq \emptyset)$
7		acni2	$⊢ (X \in \underline{AC} A \land \forall x \in A (\{y \in X \| φ\} \subseteq X \land \{y \in X \| φ\} \neq \emptyset)) \to \exists g (g : A ⟶ X \land \forall x \in A g (x) \in \{y \in X \| φ\})$
8	6 7	sylan2	$⊢ (X \in \underline{AC} A \land \forall x \in A \exists y \in X φ) \to \exists g (g : A ⟶ X \land \forall x \in A g (x) \in \{y \in X \| φ\})$
9	1	elrab	$⊢ g (x) \in \{y \in X \| φ\} \leftrightarrow (g (x) \in X \land ψ)$
10	9	simprbi	$⊢ g (x) \in \{y \in X \| φ\} \to ψ$
11	10	ralimi	$⊢ \forall x \in A g (x) \in \{y \in X \| φ\} \to \forall x \in A ψ$
12	11	anim2i	$⊢ (g : A ⟶ X \land \forall x \in A g (x) \in \{y \in X \| φ\}) \to (g : A ⟶ X \land \forall x \in A ψ)$
13	12	eximi	$⊢ \exists g (g : A ⟶ X \land \forall x \in A g (x) \in \{y \in X \| φ\}) \to \exists g (g : A ⟶ X \land \forall x \in A ψ)$
14	8 13	syl	$⊢ (X \in \underline{AC} A \land \forall x \in A \exists y \in X φ) \to \exists g (g : A ⟶ X \land \forall x \in A ψ)$

Metamath Proof Explorer