MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  aceq1 Structured version   Visualization version   GIF version

Theorem aceq1 8823
Description: Equivalence of two versions of the Axiom of Choice ax-ac 9164. 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.)
Assertion
Ref Expression
aceq1 (∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑦𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
Distinct variable group:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢

Proof of Theorem aceq1
Dummy variables 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 biidd 251 . . . . . . 7 (𝑤 = 𝑡 → (∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢)))
21cbvralv 3147 . . . . . 6 (∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢))
3 eleq1 2676 . . . . . . . . . 10 (𝑣 = 𝑧 → (𝑣𝑢𝑧𝑢))
43anbi2d 736 . . . . . . . . 9 (𝑣 = 𝑧 → ((𝑢𝑣𝑢) ↔ (𝑢𝑧𝑢)))
54rexbidv 3034 . . . . . . . 8 (𝑣 = 𝑧 → (∃𝑢𝑦 (𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝑢𝑧𝑢)))
65cbvreuv 3149 . . . . . . 7 (∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
76ralbii 2963 . . . . . 6 (∀𝑡 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
82, 7bitri 263 . . . . 5 (∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
98ralbii 2963 . . . 4 (∀𝑥𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑥𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
10 eleq1 2676 . . . . . . . . 9 (𝑧 = → (𝑧𝑢𝑢))
1110anbi1d 737 . . . . . . . 8 (𝑧 = → ((𝑧𝑢𝑣𝑢) ↔ (𝑢𝑣𝑢)))
1211rexbidv 3034 . . . . . . 7 (𝑧 = → (∃𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝑢𝑣𝑢)))
1312reueqd 3125 . . . . . 6 (𝑧 = → (∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢)))
1413raleqbi1dv 3123 . . . . 5 (𝑧 = → (∀𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢)))
1514cbvralv 3147 . . . 4 (∀𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑥𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢))
16 eleq1 2676 . . . . . . . . 9 (𝑤 = → (𝑤𝑢𝑢))
1716anbi1d 737 . . . . . . . 8 (𝑤 = → ((𝑤𝑢𝑧𝑢) ↔ (𝑢𝑧𝑢)))
1817rexbidv 3034 . . . . . . 7 (𝑤 = → (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑢𝑦 (𝑢𝑧𝑢)))
1918reueqd 3125 . . . . . 6 (𝑤 = → (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢)))
2019raleqbi1dv 3123 . . . . 5 (𝑤 = → (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢)))
2120cbvralv 3147 . . . 4 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑥𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
229, 15, 213bitr4i 291 . . 3 (∀𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢))
2322exbii 1764 . 2 (∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑦𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢))
24 19.21v 1855 . . . . . 6 (∀𝑧(𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤𝑥 → ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
25 impexp 461 . . . . . . . 8 (((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑧𝑤 → (𝑤𝑥 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
26 bi2.04 375 . . . . . . . 8 ((𝑧𝑤 → (𝑤𝑥 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
2725, 26bitri 263 . . . . . . 7 (((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
2827albii 1737 . . . . . 6 (∀𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑧(𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
29 df-eu 2462 . . . . . . . . . . 11 (∃!𝑧(𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ ∃𝑥𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
30 df-reu 2903 . . . . . . . . . . 11 (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃!𝑧(𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)))
31 19.42v 1905 . . . . . . . . . . . . . . 15 (∃𝑥(𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))) ↔ (𝑧𝑤 ∧ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
32 an42 862 . . . . . . . . . . . . . . . . 17 (((𝑧𝑤𝑥𝑦) ∧ (𝑤𝑥𝑧𝑥)) ↔ ((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)))
33 anass 679 . . . . . . . . . . . . . . . . 17 (((𝑧𝑤𝑥𝑦) ∧ (𝑤𝑥𝑧𝑥)) ↔ (𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
3432, 33bitr3i 265 . . . . . . . . . . . . . . . 16 (((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ (𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
3534exbii 1764 . . . . . . . . . . . . . . 15 (∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ ∃𝑥(𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
36 df-rex 2902 . . . . . . . . . . . . . . . . 17 (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑢(𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)))
37 eleq1 2676 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → (𝑢𝑦𝑥𝑦))
38 eleq2 2677 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑥 → (𝑤𝑢𝑤𝑥))
39 eleq2 2677 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑥 → (𝑧𝑢𝑧𝑥))
4038, 39anbi12d 743 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → ((𝑤𝑢𝑧𝑢) ↔ (𝑤𝑥𝑧𝑥)))
4137, 40anbi12d 743 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → ((𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)) ↔ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
4241cbvexv 2263 . . . . . . . . . . . . . . . . 17 (∃𝑢(𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)) ↔ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥)))
4336, 42bitri 263 . . . . . . . . . . . . . . . 16 (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥)))
4443anbi2i 726 . . . . . . . . . . . . . . 15 ((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑧𝑤 ∧ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
4531, 35, 443bitr4i 291 . . . . . . . . . . . . . 14 (∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ (𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)))
4645bibi1i 327 . . . . . . . . . . . . 13 ((∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4746albii 1737 . . . . . . . . . . . 12 (∀𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ∀𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4847exbii 1764 . . . . . . . . . . 11 (∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ∃𝑥𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4929, 30, 483bitr4i 291 . . . . . . . . . 10 (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
5049imbi2i 325 . . . . . . . . 9 ((𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
5150albii 1737 . . . . . . . 8 (∀𝑡(𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ ∀𝑡(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
52 df-ral 2901 . . . . . . . 8 (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑡(𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
53 nfv 1830 . . . . . . . . 9 𝑡(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
54 nfv 1830 . . . . . . . . . 10 𝑧 𝑡𝑤
55 nfa1 2015 . . . . . . . . . . 11 𝑧𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)
5655nfex 2140 . . . . . . . . . 10 𝑧𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)
5754, 56nfim 1813 . . . . . . . . 9 𝑧(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
58 eleq1 2676 . . . . . . . . . 10 (𝑧 = 𝑡 → (𝑧𝑤𝑡𝑤))
5958imbi1d 330 . . . . . . . . 9 (𝑧 = 𝑡 → ((𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
6053, 57, 59cbval 2259 . . . . . . . 8 (∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑡(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6151, 52, 603bitr4i 291 . . . . . . 7 (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6261imbi2i 325 . . . . . 6 ((𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑤𝑥 → ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
6324, 28, 623bitr4i 291 . . . . 5 (∀𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
6463albii 1737 . . . 4 (∀𝑤𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤(𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
65 alcom 2024 . . . 4 (∀𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
66 df-ral 2901 . . . 4 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑤(𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
6764, 65, 663bitr4ri 292 . . 3 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6867exbii 1764 . 2 (∃𝑦𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑦𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6923, 68bitri 263 1 (∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑦𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  wal 1473  wex 1695  ∃!weu 2458  wral 2896  wrex 2897  ∃!wreu 2898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-reu 2903
This theorem is referenced by:  aceq0  8824  dfac1  8839
  Copyright terms: Public domain W3C validator