Metamath Proof Explorer

Theorem 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 ⊢∃y∀z∈x∀w∈z∃!v∈z∃u∈yz∈u∧v∈u↔∃y∀z∀wz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x

Proof

Step Hyp Ref Expression
1 biidd ⊢w=t→∃!v∈h∃u∈yh∈u∧v∈u↔∃!v∈h∃u∈yh∈u∧v∈u
2 1 cbvralvw ⊢∀w∈h∃!v∈h∃u∈yh∈u∧v∈u↔∀t∈h∃!v∈h∃u∈yh∈u∧v∈u
3 elequ1 ⊢v=z→v∈u↔z∈u
4 3 anbi2d ⊢v=z→h∈u∧v∈u↔h∈u∧z∈u
5 4 rexbidv ⊢v=z→∃u∈yh∈u∧v∈u↔∃u∈yh∈u∧z∈u
6 5 cbvreuvw ⊢∃!v∈h∃u∈yh∈u∧v∈u↔∃!z∈h∃u∈yh∈u∧z∈u
7 6 ralbii ⊢∀t∈h∃!v∈h∃u∈yh∈u∧v∈u↔∀t∈h∃!z∈h∃u∈yh∈u∧z∈u
8 2 7 bitri ⊢∀w∈h∃!v∈h∃u∈yh∈u∧v∈u↔∀t∈h∃!z∈h∃u∈yh∈u∧z∈u
9 8 ralbii ⊢∀h∈x∀w∈h∃!v∈h∃u∈yh∈u∧v∈u↔∀h∈x∀t∈h∃!z∈h∃u∈yh∈u∧z∈u
10 elequ1 ⊢z=h→z∈u↔h∈u
11 10 anbi1d ⊢z=h→z∈u∧v∈u↔h∈u∧v∈u
12 11 rexbidv ⊢z=h→∃u∈yz∈u∧v∈u↔∃u∈yh∈u∧v∈u
13 12 reueqd ⊢z=h→∃!v∈z∃u∈yz∈u∧v∈u↔∃!v∈h∃u∈yh∈u∧v∈u
14 13 raleqbi1dv ⊢z=h→∀w∈z∃!v∈z∃u∈yz∈u∧v∈u↔∀w∈h∃!v∈h∃u∈yh∈u∧v∈u
15 14 cbvralvw ⊢∀z∈x∀w∈z∃!v∈z∃u∈yz∈u∧v∈u↔∀h∈x∀w∈h∃!v∈h∃u∈yh∈u∧v∈u
16 elequ1 ⊢w=h→w∈u↔h∈u
17 16 anbi1d ⊢w=h→w∈u∧z∈u↔h∈u∧z∈u
18 17 rexbidv ⊢w=h→∃u∈yw∈u∧z∈u↔∃u∈yh∈u∧z∈u
19 18 reueqd ⊢w=h→∃!z∈w∃u∈yw∈u∧z∈u↔∃!z∈h∃u∈yh∈u∧z∈u
20 19 raleqbi1dv ⊢w=h→∀t∈w∃!z∈w∃u∈yw∈u∧z∈u↔∀t∈h∃!z∈h∃u∈yh∈u∧z∈u
21 20 cbvralvw ⊢∀w∈x∀t∈w∃!z∈w∃u∈yw∈u∧z∈u↔∀h∈x∀t∈h∃!z∈h∃u∈yh∈u∧z∈u
22 9 15 21 3bitr4i ⊢∀z∈x∀w∈z∃!v∈z∃u∈yz∈u∧v∈u↔∀w∈x∀t∈w∃!z∈w∃u∈yw∈u∧z∈u
23 22 exbii ⊢∃y∀z∈x∀w∈z∃!v∈z∃u∈yz∈u∧v∈u↔∃y∀w∈x∀t∈w∃!z∈w∃u∈yw∈u∧z∈u
24 19.21v ⊢∀zw∈x→z∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x↔w∈x→∀zz∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
25 impexp ⊢z∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x↔z∈w→w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
26 bi2.04 ⊢z∈w→w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x↔w∈x→z∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
27 25 26 bitri ⊢z∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x↔w∈x→z∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
28 27 albii ⊢∀zz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x↔∀zw∈x→z∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
29 eu6 ⊢∃!zz∈w∧∃u∈yw∈u∧z∈u↔∃x∀zz∈w∧∃u∈yw∈u∧z∈u↔z=x
30 df-reu ⊢∃!z∈w∃u∈yw∈u∧z∈u↔∃!zz∈w∧∃u∈yw∈u∧z∈u
31 19.42v ⊢∃xz∈w∧x∈y∧w∈x∧z∈x↔z∈w∧∃xx∈y∧w∈x∧z∈x
32 an42 ⊢z∈w∧x∈y∧w∈x∧z∈x↔z∈w∧w∈x∧z∈x∧x∈y
33 anass ⊢z∈w∧x∈y∧w∈x∧z∈x↔z∈w∧x∈y∧w∈x∧z∈x
34 32 33 bitr3i ⊢z∈w∧w∈x∧z∈x∧x∈y↔z∈w∧x∈y∧w∈x∧z∈x
35 34 exbii ⊢∃xz∈w∧w∈x∧z∈x∧x∈y↔∃xz∈w∧x∈y∧w∈x∧z∈x
36 df-rex ⊢∃u∈yw∈u∧z∈u↔∃uu∈y∧w∈u∧z∈u
37 elequ1 ⊢u=x→u∈y↔x∈y
38 elequ2 ⊢u=x→w∈u↔w∈x
39 elequ2 ⊢u=x→z∈u↔z∈x
40 38 39 anbi12d ⊢u=x→w∈u∧z∈u↔w∈x∧z∈x
41 37 40 anbi12d ⊢u=x→u∈y∧w∈u∧z∈u↔x∈y∧w∈x∧z∈x
42 41 cbvexvw ⊢∃uu∈y∧w∈u∧z∈u↔∃xx∈y∧w∈x∧z∈x
43 36 42 bitri ⊢∃u∈yw∈u∧z∈u↔∃xx∈y∧w∈x∧z∈x
44 43 anbi2i ⊢z∈w∧∃u∈yw∈u∧z∈u↔z∈w∧∃xx∈y∧w∈x∧z∈x
45 31 35 44 3bitr4i ⊢∃xz∈w∧w∈x∧z∈x∧x∈y↔z∈w∧∃u∈yw∈u∧z∈u
46 45 bibi1i ⊢∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x↔z∈w∧∃u∈yw∈u∧z∈u↔z=x
47 46 albii ⊢∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x↔∀zz∈w∧∃u∈yw∈u∧z∈u↔z=x
48 47 exbii ⊢∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x↔∃x∀zz∈w∧∃u∈yw∈u∧z∈u↔z=x
49 29 30 48 3bitr4i ⊢∃!z∈w∃u∈yw∈u∧z∈u↔∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
50 49 imbi2i ⊢t∈w→∃!z∈w∃u∈yw∈u∧z∈u↔t∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
51 50 albii ⊢∀tt∈w→∃!z∈w∃u∈yw∈u∧z∈u↔∀tt∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
52 df-ral ⊢∀t∈w∃!z∈w∃u∈yw∈u∧z∈u↔∀tt∈w→∃!z∈w∃u∈yw∈u∧z∈u
53 nfv ⊢Ⅎtz∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
54 nfv ⊢Ⅎzt∈w
55 nfa1 ⊢Ⅎz∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
56 55 nfex ⊢Ⅎz∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
57 54 56 nfim ⊢Ⅎzt∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
58 elequ1 ⊢z=t→z∈w↔t∈w
59 58 imbi1d ⊢z=t→z∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x↔t∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
60 53 57 59 cbvalv1 ⊢∀zz∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x↔∀tt∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
61 51 52 60 3bitr4i ⊢∀t∈w∃!z∈w∃u∈yw∈u∧z∈u↔∀zz∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
62 61 imbi2i ⊢w∈x→∀t∈w∃!z∈w∃u∈yw∈u∧z∈u↔w∈x→∀zz∈w→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
63 24 28 62 3bitr4i ⊢∀zz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x↔w∈x→∀t∈w∃!z∈w∃u∈yw∈u∧z∈u
64 63 albii ⊢∀w∀zz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x↔∀ww∈x→∀t∈w∃!z∈w∃u∈yw∈u∧z∈u
65 alcom ⊢∀z∀wz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x↔∀w∀zz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
66 df-ral ⊢∀w∈x∀t∈w∃!z∈w∃u∈yw∈u∧z∈u↔∀ww∈x→∀t∈w∃!z∈w∃u∈yw∈u∧z∈u
67 64 65 66 3bitr4ri ⊢∀w∈x∀t∈w∃!z∈w∃u∈yw∈u∧z∈u↔∀z∀wz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
68 67 exbii ⊢∃y∀w∈x∀t∈w∃!z∈w∃u∈yw∈u∧z∈u↔∃y∀z∀wz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x
69 23 68 bitri ⊢∃y∀z∈x∀w∈z∃!v∈z∃u∈yz∈u∧v∈u↔∃y∀z∀wz∈w∧w∈x→∃x∀z∃xz∈w∧w∈x∧z∈x∧x∈y↔z=x