This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ac6s

Description: Equivalent of Axiom of Choice. Using the Boundedness Axiom bnd2 , we derive this strong version of ac6 that doesn't require B to be a set. (Contributed by NM, 4-Feb-2004)

		Ref	Expression
	Hypotheses	ac6s.1	$⊢ A \in V$
		ac6s.2	$⊢ y = f (x) \to (φ \leftrightarrow ψ)$
	Assertion	ac6s	$⊢ \forall x \in A \exists y \in B φ \to \exists f (f : A ⟶ B \land \forall x \in A ψ)$

Proof

Step	Hyp	Ref	Expression
1		ac6s.1	$⊢ A \in V$
2		ac6s.2	$⊢ y = f (x) \to (φ \leftrightarrow ψ)$
3	1	bnd2	$⊢ \forall x \in A \exists y \in B φ \to \exists z (z \subseteq B \land \forall x \in A \exists y \in z φ)$
4		vex	$⊢ z \in V$
5	1 4 2	ac6	$⊢ \forall x \in A \exists y \in z φ \to \exists f (f : A ⟶ z \land \forall x \in A ψ)$
6	5	anim2i	$⊢ (z \subseteq B \land \forall x \in A \exists y \in z φ) \to (z \subseteq B \land \exists f (f : A ⟶ z \land \forall x \in A ψ))$
7	6	eximi	$⊢ \exists z (z \subseteq B \land \forall x \in A \exists y \in z φ) \to \exists z (z \subseteq B \land \exists f (f : A ⟶ z \land \forall x \in A ψ))$
8		fss	$⊢ (f : A ⟶ z \land z \subseteq B) \to f : A ⟶ B$
9	8	expcom	$⊢ z \subseteq B \to (f : A ⟶ z \to f : A ⟶ B)$
10	9	anim1d	$⊢ z \subseteq B \to ((f : A ⟶ z \land \forall x \in A ψ) \to (f : A ⟶ B \land \forall x \in A ψ))$
11	10	eximdv	$⊢ z \subseteq B \to (\exists f (f : A ⟶ z \land \forall x \in A ψ) \to \exists f (f : A ⟶ B \land \forall x \in A ψ))$
12	11	imp	$⊢ (z \subseteq B \land \exists f (f : A ⟶ z \land \forall x \in A ψ)) \to \exists f (f : A ⟶ B \land \forall x \in A ψ)$
13	12	exlimiv	$⊢ \exists z (z \subseteq B \land \exists f (f : A ⟶ z \land \forall x \in A ψ)) \to \exists f (f : A ⟶ B \land \forall x \in A ψ)$
14	3 7 13	3syl	$⊢ \forall x \in A \exists y \in B φ \to \exists f (f : A ⟶ B \land \forall x \in A ψ)$