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

Theorem aceq1 8884
Description: Equivalence of two versions of the Axiom of Choice ax-ac 9225. 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 252 . . . . . . 7 (𝑤 = 𝑡 → (∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢)))
21cbvralv 3159 . . . . . 6 (∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢))
3 eleq1 2686 . . . . . . . . . 10 (𝑣 = 𝑧 → (𝑣𝑢𝑧𝑢))
43anbi2d 739 . . . . . . . . 9 (𝑣 = 𝑧 → ((𝑢𝑣𝑢) ↔ (𝑢𝑧𝑢)))
54rexbidv 3045 . . . . . . . 8 (𝑣 = 𝑧 → (∃𝑢𝑦 (𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝑢𝑧𝑢)))
65cbvreuv 3161 . . . . . . 7 (∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
76ralbii 2974 . . . . . 6 (∀𝑡 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
82, 7bitri 264 . . . . 5 (∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
98ralbii 2974 . . . 4 (∀𝑥𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑥𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
10 eleq1 2686 . . . . . . . . 9 (𝑧 = → (𝑧𝑢𝑢))
1110anbi1d 740 . . . . . . . 8 (𝑧 = → ((𝑧𝑢𝑣𝑢) ↔ (𝑢𝑣𝑢)))
1211rexbidv 3045 . . . . . . 7 (𝑧 = → (∃𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝑢𝑣𝑢)))
1312reueqd 3137 . . . . . 6 (𝑧 = → (∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢)))
1413raleqbi1dv 3135 . . . . 5 (𝑧 = → (∀𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢)))
1514cbvralv 3159 . . . 4 (∀𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑥𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢))
16 eleq1 2686 . . . . . . . . 9 (𝑤 = → (𝑤𝑢𝑢))
1716anbi1d 740 . . . . . . . 8 (𝑤 = → ((𝑤𝑢𝑧𝑢) ↔ (𝑢𝑧𝑢)))
1817rexbidv 3045 . . . . . . 7 (𝑤 = → (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑢𝑦 (𝑢𝑧𝑢)))
1918reueqd 3137 . . . . . 6 (𝑤 = → (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢)))
2019raleqbi1dv 3135 . . . . 5 (𝑤 = → (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢)))
2120cbvralv 3159 . . . 4 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑥𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
229, 15, 213bitr4i 292 . . 3 (∀𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢))
2322exbii 1771 . 2 (∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑦𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢))
24 19.21v 1865 . . . . . 6 (∀𝑧(𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤𝑥 → ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
25 impexp 462 . . . . . . . 8 (((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑧𝑤 → (𝑤𝑥 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
26 bi2.04 376 . . . . . . . 8 ((𝑧𝑤 → (𝑤𝑥 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
2725, 26bitri 264 . . . . . . 7 (((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
2827albii 1744 . . . . . 6 (∀𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑧(𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
29 df-eu 2473 . . . . . . . . . . 11 (∃!𝑧(𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ ∃𝑥𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
30 df-reu 2914 . . . . . . . . . . 11 (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃!𝑧(𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)))
31 19.42v 1915 . . . . . . . . . . . . . . 15 (∃𝑥(𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))) ↔ (𝑧𝑤 ∧ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
32 an42 865 . . . . . . . . . . . . . . . . 17 (((𝑧𝑤𝑥𝑦) ∧ (𝑤𝑥𝑧𝑥)) ↔ ((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)))
33 anass 680 . . . . . . . . . . . . . . . . 17 (((𝑧𝑤𝑥𝑦) ∧ (𝑤𝑥𝑧𝑥)) ↔ (𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
3432, 33bitr3i 266 . . . . . . . . . . . . . . . 16 (((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ (𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
3534exbii 1771 . . . . . . . . . . . . . . 15 (∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ ∃𝑥(𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
36 df-rex 2913 . . . . . . . . . . . . . . . . 17 (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑢(𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)))
37 eleq1 2686 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → (𝑢𝑦𝑥𝑦))
38 elequ2 2001 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑥 → (𝑤𝑢𝑤𝑥))
39 elequ2 2001 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑥 → (𝑧𝑢𝑧𝑥))
4038, 39anbi12d 746 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → ((𝑤𝑢𝑧𝑢) ↔ (𝑤𝑥𝑧𝑥)))
4137, 40anbi12d 746 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → ((𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)) ↔ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
4241cbvexv 2274 . . . . . . . . . . . . . . . . 17 (∃𝑢(𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)) ↔ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥)))
4336, 42bitri 264 . . . . . . . . . . . . . . . 16 (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥)))
4443anbi2i 729 . . . . . . . . . . . . . . 15 ((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑧𝑤 ∧ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
4531, 35, 443bitr4i 292 . . . . . . . . . . . . . 14 (∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ (𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)))
4645bibi1i 328 . . . . . . . . . . . . 13 ((∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4746albii 1744 . . . . . . . . . . . 12 (∀𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ∀𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4847exbii 1771 . . . . . . . . . . 11 (∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ∃𝑥𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4929, 30, 483bitr4i 292 . . . . . . . . . 10 (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
5049imbi2i 326 . . . . . . . . 9 ((𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
5150albii 1744 . . . . . . . 8 (∀𝑡(𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ ∀𝑡(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
52 df-ral 2912 . . . . . . . 8 (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑡(𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
53 nfv 1840 . . . . . . . . 9 𝑡(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
54 nfv 1840 . . . . . . . . . 10 𝑧 𝑡𝑤
55 nfa1 2025 . . . . . . . . . . 11 𝑧𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)
5655nfex 2151 . . . . . . . . . 10 𝑧𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)
5754, 56nfim 1822 . . . . . . . . 9 𝑧(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
58 eleq1 2686 . . . . . . . . . 10 (𝑧 = 𝑡 → (𝑧𝑤𝑡𝑤))
5958imbi1d 331 . . . . . . . . 9 (𝑧 = 𝑡 → ((𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
6053, 57, 59cbval 2270 . . . . . . . 8 (∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑡(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6151, 52, 603bitr4i 292 . . . . . . 7 (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6261imbi2i 326 . . . . . 6 ((𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑤𝑥 → ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
6324, 28, 623bitr4i 292 . . . . 5 (∀𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
6463albii 1744 . . . 4 (∀𝑤𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤(𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
65 alcom 2034 . . . 4 (∀𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
66 df-ral 2912 . . . 4 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑤(𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
6764, 65, 663bitr4ri 293 . . 3 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6867exbii 1771 . 2 (∃𝑦𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑦𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6923, 68bitri 264 1 (∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑦𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1478  wex 1701  ∃!weu 2469  wral 2907  wrex 2908  ∃!wreu 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-reu 2914
This theorem is referenced by:  aceq0  8885  dfac1  8900
  Copyright terms: Public domain W3C validator