aceq0

Description: Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. The right-hand side is our original ax-ac . (Contributed by NM, 5-Apr-2004)

		Ref	Expression
	Assertion	aceq0	$⊢ \exists y \forall z \in x \forall w \in z \exists! v \in z \exists u \in y (z \in u \land v \in u) \leftrightarrow \exists y \forall z \forall w ((z \in w \land w \in x) \to \exists v \forall u (\exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow u = v))$

Proof

Step	Hyp	Ref	Expression
1		aceq1	$⊢ \exists y \forall z \in x \forall w \in z \exists! v \in z \exists u \in y (z \in u \land v \in u) \leftrightarrow \exists y \forall z \forall w ((z \in w \land w \in x) \to \exists x \forall z (\exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow z = x))$
2		equequ2	$⊢ v = x \to (u = v \leftrightarrow u = x)$
3	2	bibi2d	$⊢ v = x \to ((\exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow u = v) \leftrightarrow (\exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow u = x))$
4		elequ2	$⊢ t = x \to (w \in t \leftrightarrow w \in x)$
5	4	anbi2d	$⊢ t = x \to ((u \in w \land w \in t) \leftrightarrow (u \in w \land w \in x))$
6		elequ2	$⊢ t = x \to (u \in t \leftrightarrow u \in x)$
7		elequ1	$⊢ t = x \to (t \in y \leftrightarrow x \in y)$
8	6 7	anbi12d	$⊢ t = x \to ((u \in t \land t \in y) \leftrightarrow (u \in x \land x \in y))$
9	5 8	anbi12d	$⊢ t = x \to (((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow ((u \in w \land w \in x) \land (u \in x \land x \in y)))$
10	9	cbvexvw	$⊢ \exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow \exists x ((u \in w \land w \in x) \land (u \in x \land x \in y))$
11	10	bibi1i	$⊢ (\exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow u = x) \leftrightarrow (\exists x ((u \in w \land w \in x) \land (u \in x \land x \in y)) \leftrightarrow u = x)$
12	3 11	bitrdi	$⊢ v = x \to ((\exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow u = v) \leftrightarrow (\exists x ((u \in w \land w \in x) \land (u \in x \land x \in y)) \leftrightarrow u = x))$
13	12	albidv	$⊢ v = x \to (\forall u (\exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow u = v) \leftrightarrow \forall u (\exists x ((u \in w \land w \in x) \land (u \in x \land x \in y)) \leftrightarrow u = x))$
14		elequ1	$⊢ u = z \to (u \in w \leftrightarrow z \in w)$
15	14	anbi1d	$⊢ u = z \to ((u \in w \land w \in x) \leftrightarrow (z \in w \land w \in x))$
16		elequ1	$⊢ u = z \to (u \in x \leftrightarrow z \in x)$
17	16	anbi1d	$⊢ u = z \to ((u \in x \land x \in y) \leftrightarrow (z \in x \land x \in y))$
18	15 17	anbi12d	$⊢ u = z \to (((u \in w \land w \in x) \land (u \in x \land x \in y)) \leftrightarrow ((z \in w \land w \in x) \land (z \in x \land x \in y)))$
19	18	exbidv	$⊢ u = z \to (\exists x ((u \in w \land w \in x) \land (u \in x \land x \in y)) \leftrightarrow \exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)))$
20		equequ1	$⊢ u = z \to (u = x \leftrightarrow z = x)$
21	19 20	bibi12d	$⊢ u = z \to ((\exists x ((u \in w \land w \in x) \land (u \in x \land x \in y)) \leftrightarrow u = x) \leftrightarrow (\exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow z = x))$
22	21	cbvalvw	$⊢ \forall u (\exists x ((u \in w \land w \in x) \land (u \in x \land x \in y)) \leftrightarrow u = x) \leftrightarrow \forall z (\exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow z = x)$
23	13 22	bitrdi	$⊢ v = x \to (\forall u (\exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow u = v) \leftrightarrow \forall z (\exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow z = x))$
24	23	cbvexvw	$⊢ \exists v \forall u (\exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow u = v) \leftrightarrow \exists x \forall z (\exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow z = x)$
25	24	imbi2i	$⊢ ((z \in w \land w \in x) \to \exists v \forall u (\exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow u = v)) \leftrightarrow ((z \in w \land w \in x) \to \exists x \forall z (\exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow z = x))$
26	25	2albii	$⊢ \forall z \forall w ((z \in w \land w \in x) \to \exists v \forall u (\exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow u = v)) \leftrightarrow \forall z \forall w ((z \in w \land w \in x) \to \exists x \forall z (\exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow z = x))$
27	26	exbii	$⊢ \exists y \forall z \forall w ((z \in w \land w \in x) \to \exists v \forall u (\exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow u = v)) \leftrightarrow \exists y \forall z \forall w ((z \in w \land w \in x) \to \exists x \forall z (\exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow z = x))$
28	1 27	bitr4i	$⊢ \exists y \forall z \in x \forall w \in z \exists! v \in z \exists u \in y (z \in u \land v \in u) \leftrightarrow \exists y \forall z \forall w ((z \in w \land w \in x) \to \exists v \forall u (\exists t ((u \in w \land w \in t) \land (u \in t \land t \in y)) \leftrightarrow u = v))$

Metamath Proof Explorer

Theorem aceq0

Proof