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

Theorem aceq1 8978
Description: Equivalence of two versions of the Axiom of Choice ax-ac 9319. 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 3201 . . . . . 6 (∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢))
3 eleq1 2718 . . . . . . . . . 10 (𝑣 = 𝑧 → (𝑣𝑢𝑧𝑢))
43anbi2d 740 . . . . . . . . 9 (𝑣 = 𝑧 → ((𝑢𝑣𝑢) ↔ (𝑢𝑧𝑢)))
54rexbidv 3081 . . . . . . . 8 (𝑣 = 𝑧 → (∃𝑢𝑦 (𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝑢𝑧𝑢)))
65cbvreuv 3203 . . . . . . 7 (∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
76ralbii 3009 . . . . . 6 (∀𝑡 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
82, 7bitri 264 . . . . 5 (∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
98ralbii 3009 . . . 4 (∀𝑥𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑥𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
10 eleq1 2718 . . . . . . . . 9 (𝑧 = → (𝑧𝑢𝑢))
1110anbi1d 741 . . . . . . . 8 (𝑧 = → ((𝑧𝑢𝑣𝑢) ↔ (𝑢𝑣𝑢)))
1211rexbidv 3081 . . . . . . 7 (𝑧 = → (∃𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝑢𝑣𝑢)))
1312reueqd 3178 . . . . . 6 (𝑧 = → (∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢)))
1413raleqbi1dv 3176 . . . . 5 (𝑧 = → (∀𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢)))
1514cbvralv 3201 . . . 4 (∀𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑥𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢))
16 eleq1 2718 . . . . . . . . 9 (𝑤 = → (𝑤𝑢𝑢))
1716anbi1d 741 . . . . . . . 8 (𝑤 = → ((𝑤𝑢𝑧𝑢) ↔ (𝑢𝑧𝑢)))
1817rexbidv 3081 . . . . . . 7 (𝑤 = → (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑢𝑦 (𝑢𝑧𝑢)))
1918reueqd 3178 . . . . . 6 (𝑤 = → (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢)))
2019raleqbi1dv 3176 . . . . 5 (𝑤 = → (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢)))
2120cbvralv 3201 . . . 4 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑥𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
229, 15, 213bitr4i 292 . . 3 (∀𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢))
2322exbii 1814 . 2 (∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑦𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢))
24 19.21v 1908 . . . . . 6 (∀𝑧(𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤𝑥 → ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
25 impexp 461 . . . . . . . 8 (((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑧𝑤 → (𝑤𝑥 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
26 bi2.04 375 . . . . . . . 8 ((𝑧𝑤 → (𝑤𝑥 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
2725, 26bitri 264 . . . . . . 7 (((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
2827albii 1787 . . . . . 6 (∀𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑧(𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
29 df-eu 2502 . . . . . . . . . . 11 (∃!𝑧(𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ ∃𝑥𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
30 df-reu 2948 . . . . . . . . . . 11 (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃!𝑧(𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)))
31 19.42v 1921 . . . . . . . . . . . . . . 15 (∃𝑥(𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))) ↔ (𝑧𝑤 ∧ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
32 an42 883 . . . . . . . . . . . . . . . . 17 (((𝑧𝑤𝑥𝑦) ∧ (𝑤𝑥𝑧𝑥)) ↔ ((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)))
33 anass 682 . . . . . . . . . . . . . . . . 17 (((𝑧𝑤𝑥𝑦) ∧ (𝑤𝑥𝑧𝑥)) ↔ (𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
3432, 33bitr3i 266 . . . . . . . . . . . . . . . 16 (((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ (𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
3534exbii 1814 . . . . . . . . . . . . . . 15 (∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ ∃𝑥(𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
36 df-rex 2947 . . . . . . . . . . . . . . . . 17 (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑢(𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)))
37 eleq1 2718 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → (𝑢𝑦𝑥𝑦))
38 elequ2 2044 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑥 → (𝑤𝑢𝑤𝑥))
39 elequ2 2044 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑥 → (𝑧𝑢𝑧𝑥))
4038, 39anbi12d 747 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → ((𝑤𝑢𝑧𝑢) ↔ (𝑤𝑥𝑧𝑥)))
4137, 40anbi12d 747 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → ((𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)) ↔ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
4241cbvexv 2311 . . . . . . . . . . . . . . . . 17 (∃𝑢(𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)) ↔ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥)))
4336, 42bitri 264 . . . . . . . . . . . . . . . 16 (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥)))
4443anbi2i 730 . . . . . . . . . . . . . . 15 ((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑧𝑤 ∧ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
4531, 35, 443bitr4i 292 . . . . . . . . . . . . . 14 (∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ (𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)))
4645bibi1i 327 . . . . . . . . . . . . 13 ((∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4746albii 1787 . . . . . . . . . . . 12 (∀𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ∀𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4847exbii 1814 . . . . . . . . . . 11 (∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ∃𝑥𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4929, 30, 483bitr4i 292 . . . . . . . . . 10 (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
5049imbi2i 325 . . . . . . . . 9 ((𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
5150albii 1787 . . . . . . . 8 (∀𝑡(𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ ∀𝑡(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
52 df-ral 2946 . . . . . . . 8 (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑡(𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
53 nfv 1883 . . . . . . . . 9 𝑡(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
54 nfv 1883 . . . . . . . . . 10 𝑧 𝑡𝑤
55 nfa1 2068 . . . . . . . . . . 11 𝑧𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)
5655nfex 2192 . . . . . . . . . 10 𝑧𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)
5754, 56nfim 1865 . . . . . . . . 9 𝑧(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
58 eleq1 2718 . . . . . . . . . 10 (𝑧 = 𝑡 → (𝑧𝑤𝑡𝑤))
5958imbi1d 330 . . . . . . . . 9 (𝑧 = 𝑡 → ((𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
6053, 57, 59cbval 2307 . . . . . . . 8 (∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑡(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6151, 52, 603bitr4i 292 . . . . . . 7 (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6261imbi2i 325 . . . . . 6 ((𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑤𝑥 → ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
6324, 28, 623bitr4i 292 . . . . 5 (∀𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
6463albii 1787 . . . 4 (∀𝑤𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤(𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
65 alcom 2077 . . . 4 (∀𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
66 df-ral 2946 . . . 4 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑤(𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
6764, 65, 663bitr4ri 293 . . 3 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6867exbii 1814 . 2 (∃𝑦𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑦𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6923, 68bitri 264 1 (∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑦𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wal 1521  wex 1744  ∃!weu 2498  wral 2941  wrex 2942  ∃!wreu 2943
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-reu 2948
This theorem is referenced by:  aceq0  8979  dfac1  8994
  Copyright terms: Public domain W3C validator