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

Theorem aceq1 9130
 Description: Equivalence of two versions of the Axiom of Choice ax-ac 9473. 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 3310 . . . . . 6 (∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢))
3 eleq1w 2822 . . . . . . . . . 10 (𝑣 = 𝑧 → (𝑣𝑢𝑧𝑢))
43anbi2d 742 . . . . . . . . 9 (𝑣 = 𝑧 → ((𝑢𝑣𝑢) ↔ (𝑢𝑧𝑢)))
54rexbidv 3190 . . . . . . . 8 (𝑣 = 𝑧 → (∃𝑢𝑦 (𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝑢𝑧𝑢)))
65cbvreuv 3312 . . . . . . 7 (∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
76ralbii 3118 . . . . . 6 (∀𝑡 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
82, 7bitri 264 . . . . 5 (∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
98ralbii 3118 . . . 4 (∀𝑥𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑥𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
10 eleq1w 2822 . . . . . . . . 9 (𝑧 = → (𝑧𝑢𝑢))
1110anbi1d 743 . . . . . . . 8 (𝑧 = → ((𝑧𝑢𝑣𝑢) ↔ (𝑢𝑣𝑢)))
1211rexbidv 3190 . . . . . . 7 (𝑧 = → (∃𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝑢𝑣𝑢)))
1312reueqd 3287 . . . . . 6 (𝑧 = → (∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢)))
1413raleqbi1dv 3285 . . . . 5 (𝑧 = → (∀𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢)))
1514cbvralv 3310 . . . 4 (∀𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑥𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢))
16 eleq1w 2822 . . . . . . . . 9 (𝑤 = → (𝑤𝑢𝑢))
1716anbi1d 743 . . . . . . . 8 (𝑤 = → ((𝑤𝑢𝑧𝑢) ↔ (𝑢𝑧𝑢)))
1817rexbidv 3190 . . . . . . 7 (𝑤 = → (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑢𝑦 (𝑢𝑧𝑢)))
1918reueqd 3287 . . . . . 6 (𝑤 = → (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢)))
2019raleqbi1dv 3285 . . . . 5 (𝑤 = → (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢)))
2120cbvralv 3310 . . . 4 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑥𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
229, 15, 213bitr4i 292 . . 3 (∀𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢))
2322exbii 1923 . 2 (∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑦𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢))
24 19.21v 2017 . . . . . 6 (∀𝑧(𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤𝑥 → ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
25 impexp 461 . . . . . . . 8 (((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑧𝑤 → (𝑤𝑥 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
26 bi2.04 375 . . . . . . . 8 ((𝑧𝑤 → (𝑤𝑥 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
2725, 26bitri 264 . . . . . . 7 (((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
2827albii 1896 . . . . . 6 (∀𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑧(𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
29 df-eu 2611 . . . . . . . . . . 11 (∃!𝑧(𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ ∃𝑥𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
30 df-reu 3057 . . . . . . . . . . 11 (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃!𝑧(𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)))
31 19.42v 2030 . . . . . . . . . . . . . . 15 (∃𝑥(𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))) ↔ (𝑧𝑤 ∧ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
32 an42 901 . . . . . . . . . . . . . . . . 17 (((𝑧𝑤𝑥𝑦) ∧ (𝑤𝑥𝑧𝑥)) ↔ ((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)))
33 anass 684 . . . . . . . . . . . . . . . . 17 (((𝑧𝑤𝑥𝑦) ∧ (𝑤𝑥𝑧𝑥)) ↔ (𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
3432, 33bitr3i 266 . . . . . . . . . . . . . . . 16 (((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ (𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
3534exbii 1923 . . . . . . . . . . . . . . 15 (∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ ∃𝑥(𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
36 df-rex 3056 . . . . . . . . . . . . . . . . 17 (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑢(𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)))
37 eleq1w 2822 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → (𝑢𝑦𝑥𝑦))
38 elequ2 2153 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑥 → (𝑤𝑢𝑤𝑥))
39 elequ2 2153 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑥 → (𝑧𝑢𝑧𝑥))
4038, 39anbi12d 749 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → ((𝑤𝑢𝑧𝑢) ↔ (𝑤𝑥𝑧𝑥)))
4137, 40anbi12d 749 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → ((𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)) ↔ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
4241cbvexv 2420 . . . . . . . . . . . . . . . . 17 (∃𝑢(𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)) ↔ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥)))
4336, 42bitri 264 . . . . . . . . . . . . . . . 16 (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥)))
4443anbi2i 732 . . . . . . . . . . . . . . 15 ((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑧𝑤 ∧ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
4531, 35, 443bitr4i 292 . . . . . . . . . . . . . 14 (∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ (𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)))
4645bibi1i 327 . . . . . . . . . . . . 13 ((∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4746albii 1896 . . . . . . . . . . . 12 (∀𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ∀𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4847exbii 1923 . . . . . . . . . . 11 (∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ∃𝑥𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4929, 30, 483bitr4i 292 . . . . . . . . . 10 (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
5049imbi2i 325 . . . . . . . . 9 ((𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
5150albii 1896 . . . . . . . 8 (∀𝑡(𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ ∀𝑡(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
52 df-ral 3055 . . . . . . . 8 (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑡(𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
53 nfv 1992 . . . . . . . . 9 𝑡(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
54 nfv 1992 . . . . . . . . . 10 𝑧 𝑡𝑤
55 nfa1 2177 . . . . . . . . . . 11 𝑧𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)
5655nfex 2301 . . . . . . . . . 10 𝑧𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)
5754, 56nfim 1974 . . . . . . . . 9 𝑧(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
58 eleq1w 2822 . . . . . . . . . 10 (𝑧 = 𝑡 → (𝑧𝑤𝑡𝑤))
5958imbi1d 330 . . . . . . . . 9 (𝑧 = 𝑡 → ((𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
6053, 57, 59cbval 2416 . . . . . . . 8 (∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑡(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6151, 52, 603bitr4i 292 . . . . . . 7 (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6261imbi2i 325 . . . . . 6 ((𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑤𝑥 → ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
6324, 28, 623bitr4i 292 . . . . 5 (∀𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
6463albii 1896 . . . 4 (∀𝑤𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤(𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
65 alcom 2186 . . . 4 (∀𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
66 df-ral 3055 . . . 4 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑤(𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
6764, 65, 663bitr4ri 293 . . 3 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6867exbii 1923 . 2 (∃𝑦𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑦𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6923, 68bitri 264 1 (∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑦𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1630  ∃wex 1853  ∃!weu 2607  ∀wral 3050  ∃wrex 3051  ∃!wreu 3052 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-reu 3057 This theorem is referenced by:  aceq0  9131  dfac1  9148
 Copyright terms: Public domain W3C validator