aceq1

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

		Ref	Expression
	Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		biidd	$⊢ w = t \to (\exists! v \in h \exists u \in y (h \in u \land v \in u) \leftrightarrow \exists! v \in h \exists u \in y (h \in u \land v \in u))$
2	1	cbvralvw	$⊢ \forall w \in h \exists! v \in h \exists u \in y (h \in u \land v \in u) \leftrightarrow \forall t \in h \exists! v \in h \exists u \in y (h \in u \land v \in u)$
3		elequ1	$⊢ v = z \to (v \in u \leftrightarrow z \in u)$
4	3	anbi2d	$⊢ v = z \to ((h \in u \land v \in u) \leftrightarrow (h \in u \land z \in u))$
5	4	rexbidv	$⊢ v = z \to (\exists u \in y (h \in u \land v \in u) \leftrightarrow \exists u \in y (h \in u \land z \in u))$
6	5	cbvreuvw	$⊢ \exists! v \in h \exists u \in y (h \in u \land v \in u) \leftrightarrow \exists! z \in h \exists u \in y (h \in u \land z \in u)$
7	6	ralbii	$⊢ \forall t \in h \exists! v \in h \exists u \in y (h \in u \land v \in u) \leftrightarrow \forall t \in h \exists! z \in h \exists u \in y (h \in u \land z \in u)$
8	2 7	bitri	$⊢ \forall w \in h \exists! v \in h \exists u \in y (h \in u \land v \in u) \leftrightarrow \forall t \in h \exists! z \in h \exists u \in y (h \in u \land z \in u)$
9	8	ralbii	$⊢ \forall h \in x \forall w \in h \exists! v \in h \exists u \in y (h \in u \land v \in u) \leftrightarrow \forall h \in x \forall t \in h \exists! z \in h \exists u \in y (h \in u \land z \in u)$
10		elequ1	$⊢ z = h \to (z \in u \leftrightarrow h \in u)$
11	10	anbi1d	$⊢ z = h \to ((z \in u \land v \in u) \leftrightarrow (h \in u \land v \in u))$
12	11	rexbidv	$⊢ z = h \to (\exists u \in y (z \in u \land v \in u) \leftrightarrow \exists u \in y (h \in u \land v \in u))$
13	12	reueqd	$⊢ z = h \to (\exists! v \in z \exists u \in y (z \in u \land v \in u) \leftrightarrow \exists! v \in h \exists u \in y (h \in u \land v \in u))$
14	13	raleqbi1dv	$⊢ z = h \to (\forall w \in z \exists! v \in z \exists u \in y (z \in u \land v \in u) \leftrightarrow \forall w \in h \exists! v \in h \exists u \in y (h \in u \land v \in u))$
15	14	cbvralvw	$⊢ \forall z \in x \forall w \in z \exists! v \in z \exists u \in y (z \in u \land v \in u) \leftrightarrow \forall h \in x \forall w \in h \exists! v \in h \exists u \in y (h \in u \land v \in u)$
16		elequ1	$⊢ w = h \to (w \in u \leftrightarrow h \in u)$
17	16	anbi1d	$⊢ w = h \to ((w \in u \land z \in u) \leftrightarrow (h \in u \land z \in u))$
18	17	rexbidv	$⊢ w = h \to (\exists u \in y (w \in u \land z \in u) \leftrightarrow \exists u \in y (h \in u \land z \in u))$
19	18	reueqd	$⊢ w = h \to (\exists! z \in w \exists u \in y (w \in u \land z \in u) \leftrightarrow \exists! z \in h \exists u \in y (h \in u \land z \in u))$
20	19	raleqbi1dv	$⊢ w = h \to (\forall t \in w \exists! z \in w \exists u \in y (w \in u \land z \in u) \leftrightarrow \forall t \in h \exists! z \in h \exists u \in y (h \in u \land z \in u))$
21	20	cbvralvw	$⊢ \forall w \in x \forall t \in w \exists! z \in w \exists u \in y (w \in u \land z \in u) \leftrightarrow \forall h \in x \forall t \in h \exists! z \in h \exists u \in y (h \in u \land z \in u)$
22	9 15 21	3bitr4i	$⊢ \forall z \in x \forall w \in z \exists! v \in z \exists u \in y (z \in u \land v \in u) \leftrightarrow \forall w \in x \forall t \in w \exists! z \in w \exists u \in y (w \in u \land z \in u)$
23	22	exbii	$⊢ \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 w \in x \forall t \in w \exists! z \in w \exists u \in y (w \in u \land z \in u)$
24		19.21v	$⊢ \forall z (w \in x \to (z \in w \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))) \leftrightarrow (w \in x \to \forall z (z \in w \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)))$
25		impexp	$⊢ ((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)) \leftrightarrow (z \in w \to (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		bi2.04	$⊢ (z \in w \to (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))) \leftrightarrow (w \in x \to (z \in w \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	25 26	bitri	$⊢ ((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)) \leftrightarrow (w \in x \to (z \in w \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	27	albii	$⊢ \forall z ((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)) \leftrightarrow \forall z (w \in x \to (z \in w \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)))$
29		eu6	$⊢ \exists! z (z \in w \land \exists u \in y (w \in u \land z \in u)) \leftrightarrow \exists x \forall z ((z \in w \land \exists u \in y (w \in u \land z \in u)) \leftrightarrow z = x)$
30		df-reu	$⊢ \exists! z \in w \exists u \in y (w \in u \land z \in u) \leftrightarrow \exists! z (z \in w \land \exists u \in y (w \in u \land z \in u))$
31		19.42v	$⊢ \exists x (z \in w \land (x \in y \land (w \in x \land z \in x))) \leftrightarrow (z \in w \land \exists x (x \in y \land (w \in x \land z \in x)))$
32		an42	$⊢ ((z \in w \land x \in y) \land (w \in x \land z \in x)) \leftrightarrow ((z \in w \land w \in x) \land (z \in x \land x \in y))$
33		anass	$⊢ ((z \in w \land x \in y) \land (w \in x \land z \in x)) \leftrightarrow (z \in w \land (x \in y \land (w \in x \land z \in x)))$
34	32 33	bitr3i	$⊢ ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow (z \in w \land (x \in y \land (w \in x \land z \in x)))$
35	34	exbii	$⊢ \exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow \exists x (z \in w \land (x \in y \land (w \in x \land z \in x)))$
36		df-rex	$⊢ \exists u \in y (w \in u \land z \in u) \leftrightarrow \exists u (u \in y \land (w \in u \land z \in u))$
37		elequ1	$⊢ u = x \to (u \in y \leftrightarrow x \in y)$
38		elequ2	$⊢ u = x \to (w \in u \leftrightarrow w \in x)$
39		elequ2	$⊢ u = x \to (z \in u \leftrightarrow z \in x)$
40	38 39	anbi12d	$⊢ u = x \to ((w \in u \land z \in u) \leftrightarrow (w \in x \land z \in x))$
41	37 40	anbi12d	$⊢ u = x \to ((u \in y \land (w \in u \land z \in u)) \leftrightarrow (x \in y \land (w \in x \land z \in x)))$
42	41	cbvexvw	$⊢ \exists u (u \in y \land (w \in u \land z \in u)) \leftrightarrow \exists x (x \in y \land (w \in x \land z \in x))$
43	36 42	bitri	$⊢ \exists u \in y (w \in u \land z \in u) \leftrightarrow \exists x (x \in y \land (w \in x \land z \in x))$
44	43	anbi2i	$⊢ (z \in w \land \exists u \in y (w \in u \land z \in u)) \leftrightarrow (z \in w \land \exists x (x \in y \land (w \in x \land z \in x)))$
45	31 35 44	3bitr4i	$⊢ \exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow (z \in w \land \exists u \in y (w \in u \land z \in u))$
46	45	bibi1i	$⊢ (\exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow z = x) \leftrightarrow ((z \in w \land \exists u \in y (w \in u \land z \in u)) \leftrightarrow z = x)$
47	46	albii	$⊢ \forall z (\exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow z = x) \leftrightarrow \forall z ((z \in w \land \exists u \in y (w \in u \land z \in u)) \leftrightarrow z = x)$
48	47	exbii	$⊢ \exists x \forall z (\exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow z = x) \leftrightarrow \exists x \forall z ((z \in w \land \exists u \in y (w \in u \land z \in u)) \leftrightarrow z = x)$
49	29 30 48	3bitr4i	$⊢ \exists! z \in w \exists u \in y (w \in u \land z \in u) \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)$
50	49	imbi2i	$⊢ (t \in w \to \exists! z \in w \exists u \in y (w \in u \land z \in u)) \leftrightarrow (t \in w \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))$
51	50	albii	$⊢ \forall t (t \in w \to \exists! z \in w \exists u \in y (w \in u \land z \in u)) \leftrightarrow \forall t (t \in w \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))$
52		df-ral	$⊢ \forall t \in w \exists! z \in w \exists u \in y (w \in u \land z \in u) \leftrightarrow \forall t (t \in w \to \exists! z \in w \exists u \in y (w \in u \land z \in u))$
53		nfv	$⊢ Ⅎ t (z \in w \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))$
54		nfv	$⊢ Ⅎ z t \in w$
55		nfa1	$⊢ Ⅎ z \forall z (\exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow z = x)$
56	55	nfex	$⊢ Ⅎ z \exists x \forall z (\exists x ((z \in w \land w \in x) \land (z \in x \land x \in y)) \leftrightarrow z = x)$
57	54 56	nfim	$⊢ Ⅎ z (t \in w \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))$
58		elequ1	$⊢ z = t \to (z \in w \leftrightarrow t \in w)$
59	58	imbi1d	$⊢ z = t \to ((z \in w \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)) \leftrightarrow (t \in w \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)))$
60	53 57 59	cbvalv1	$⊢ \forall z (z \in w \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)) \leftrightarrow \forall t (t \in w \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))$
61	51 52 60	3bitr4i	$⊢ \forall t \in w \exists! z \in w \exists u \in y (w \in u \land z \in u) \leftrightarrow \forall z (z \in w \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))$
62	61	imbi2i	$⊢ (w \in x \to \forall t \in w \exists! z \in w \exists u \in y (w \in u \land z \in u)) \leftrightarrow (w \in x \to \forall z (z \in w \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)))$
63	24 28 62	3bitr4i	$⊢ \forall z ((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)) \leftrightarrow (w \in x \to \forall t \in w \exists! z \in w \exists u \in y (w \in u \land z \in u))$
64	63	albii	$⊢ \forall w \forall z ((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)) \leftrightarrow \forall w (w \in x \to \forall t \in w \exists! z \in w \exists u \in y (w \in u \land z \in u))$
65		alcom	$⊢ \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)) \leftrightarrow \forall w \forall z ((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))$
66		df-ral	$⊢ \forall w \in x \forall t \in w \exists! z \in w \exists u \in y (w \in u \land z \in u) \leftrightarrow \forall w (w \in x \to \forall t \in w \exists! z \in w \exists u \in y (w \in u \land z \in u))$
67	64 65 66	3bitr4ri	$⊢ \forall w \in x \forall t \in w \exists! z \in w \exists u \in y (w \in u \land z \in u) \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))$
68	67	exbii	$⊢ \exists y \forall w \in x \forall t \in w \exists! z \in w \exists u \in y (w \in u \land z \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))$
69	23 68	bitri	$⊢ \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))$

Metamath Proof Explorer

Theorem aceq1

Proof