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

Theorem aceq1 9531
Description: Equivalence of two versions of the Axiom of Choice ax-ac 9869. 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 263 . . . . . . 7 (𝑤 = 𝑡 → (∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢)))
21cbvralvw 3447 . . . . . 6 (∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢))
3 elequ1 2112 . . . . . . . . . 10 (𝑣 = 𝑧 → (𝑣𝑢𝑧𝑢))
43anbi2d 628 . . . . . . . . 9 (𝑣 = 𝑧 → ((𝑢𝑣𝑢) ↔ (𝑢𝑧𝑢)))
54rexbidv 3294 . . . . . . . 8 (𝑣 = 𝑧 → (∃𝑢𝑦 (𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝑢𝑧𝑢)))
65cbvreuvw 3449 . . . . . . 7 (∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
76ralbii 3162 . . . . . 6 (∀𝑡 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
82, 7bitri 276 . . . . 5 (∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
98ralbii 3162 . . . 4 (∀𝑥𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢) ↔ ∀𝑥𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
10 elequ1 2112 . . . . . . . . 9 (𝑧 = → (𝑧𝑢𝑢))
1110anbi1d 629 . . . . . . . 8 (𝑧 = → ((𝑧𝑢𝑣𝑢) ↔ (𝑢𝑣𝑢)))
1211rexbidv 3294 . . . . . . 7 (𝑧 = → (∃𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑢𝑦 (𝑢𝑣𝑢)))
1312reueqd 3417 . . . . . 6 (𝑧 = → (∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢)))
1413raleqbi1dv 3401 . . . . 5 (𝑧 = → (∀𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢)))
1514cbvralvw 3447 . . . 4 (∀𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑥𝑤 ∃!𝑣𝑢𝑦 (𝑢𝑣𝑢))
16 elequ1 2112 . . . . . . . . 9 (𝑤 = → (𝑤𝑢𝑢))
1716anbi1d 629 . . . . . . . 8 (𝑤 = → ((𝑤𝑢𝑧𝑢) ↔ (𝑢𝑧𝑢)))
1817rexbidv 3294 . . . . . . 7 (𝑤 = → (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑢𝑦 (𝑢𝑧𝑢)))
1918reueqd 3417 . . . . . 6 (𝑤 = → (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢)))
2019raleqbi1dv 3401 . . . . 5 (𝑤 = → (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢)))
2120cbvralvw 3447 . . . 4 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑥𝑡 ∃!𝑧𝑢𝑦 (𝑢𝑧𝑢))
229, 15, 213bitr4i 304 . . 3 (∀𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢))
2322exbii 1839 . 2 (∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑦𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢))
24 19.21v 1931 . . . . . 6 (∀𝑧(𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤𝑥 → ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
25 impexp 451 . . . . . . . 8 (((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑧𝑤 → (𝑤𝑥 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
26 bi2.04 389 . . . . . . . 8 ((𝑧𝑤 → (𝑤𝑥 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))) ↔ (𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
2725, 26bitri 276 . . . . . . 7 (((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
2827albii 1811 . . . . . 6 (∀𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑧(𝑤𝑥 → (𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
29 eu6 2652 . . . . . . . . . . 11 (∃!𝑧(𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ ∃𝑥𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
30 df-reu 3142 . . . . . . . . . . 11 (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃!𝑧(𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)))
31 19.42v 1945 . . . . . . . . . . . . . . 15 (∃𝑥(𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))) ↔ (𝑧𝑤 ∧ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
32 an42 653 . . . . . . . . . . . . . . . . 17 (((𝑧𝑤𝑥𝑦) ∧ (𝑤𝑥𝑧𝑥)) ↔ ((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)))
33 anass 469 . . . . . . . . . . . . . . . . 17 (((𝑧𝑤𝑥𝑦) ∧ (𝑤𝑥𝑧𝑥)) ↔ (𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
3432, 33bitr3i 278 . . . . . . . . . . . . . . . 16 (((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ (𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
3534exbii 1839 . . . . . . . . . . . . . . 15 (∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ ∃𝑥(𝑧𝑤 ∧ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
36 df-rex 3141 . . . . . . . . . . . . . . . . 17 (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑢(𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)))
37 elequ1 2112 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → (𝑢𝑦𝑥𝑦))
38 elequ2 2120 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑥 → (𝑤𝑢𝑤𝑥))
39 elequ2 2120 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = 𝑥 → (𝑧𝑢𝑧𝑥))
4038, 39anbi12d 630 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → ((𝑤𝑢𝑧𝑢) ↔ (𝑤𝑥𝑧𝑥)))
4137, 40anbi12d 630 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → ((𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)) ↔ (𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
4241cbvexvw 2035 . . . . . . . . . . . . . . . . 17 (∃𝑢(𝑢𝑦 ∧ (𝑤𝑢𝑧𝑢)) ↔ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥)))
4336, 42bitri 276 . . . . . . . . . . . . . . . 16 (∃𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥)))
4443anbi2i 622 . . . . . . . . . . . . . . 15 ((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑧𝑤 ∧ ∃𝑥(𝑥𝑦 ∧ (𝑤𝑥𝑧𝑥))))
4531, 35, 443bitr4i 304 . . . . . . . . . . . . . 14 (∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ (𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)))
4645bibi1i 340 . . . . . . . . . . . . 13 ((∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4746albii 1811 . . . . . . . . . . . 12 (∀𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ∀𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4847exbii 1839 . . . . . . . . . . 11 (∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥) ↔ ∃𝑥𝑧((𝑧𝑤 ∧ ∃𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ 𝑧 = 𝑥))
4929, 30, 483bitr4i 304 . . . . . . . . . 10 (∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
5049imbi2i 337 . . . . . . . . 9 ((𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
5150albii 1811 . . . . . . . 8 (∀𝑡(𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ ∀𝑡(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
52 df-ral 3140 . . . . . . . 8 (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑡(𝑡𝑤 → ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
53 nfv 1906 . . . . . . . . 9 𝑡(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
54 nfv 1906 . . . . . . . . . 10 𝑧 𝑡𝑤
55 nfa1 2146 . . . . . . . . . . 11 𝑧𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)
5655nfex 2334 . . . . . . . . . 10 𝑧𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)
5754, 56nfim 1888 . . . . . . . . 9 𝑧(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))
58 elequ1 2112 . . . . . . . . . 10 (𝑧 = 𝑡 → (𝑧𝑤𝑡𝑤))
5958imbi1d 343 . . . . . . . . 9 (𝑧 = 𝑡 → ((𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
6053, 57, 59cbvalv1 2352 . . . . . . . 8 (∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑡(𝑡𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6151, 52, 603bitr4i 304 . . . . . . 7 (∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6261imbi2i 337 . . . . . 6 ((𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)) ↔ (𝑤𝑥 → ∀𝑧(𝑧𝑤 → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥))))
6324, 28, 623bitr4i 304 . . . . 5 (∀𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ (𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
6463albii 1811 . . . 4 (∀𝑤𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤(𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
65 alcom 2153 . . . 4 (∀𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)) ↔ ∀𝑤𝑧((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
66 df-ral 3140 . . . 4 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑤(𝑤𝑥 → ∀𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢)))
6764, 65, 663bitr4ri 305 . . 3 (∀𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∀𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6867exbii 1839 . 2 (∃𝑦𝑤𝑥𝑡𝑤 ∃!𝑧𝑤𝑢𝑦 (𝑤𝑢𝑧𝑢) ↔ ∃𝑦𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
6923, 68bitri 276 1 (∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃𝑦𝑧𝑤((𝑧𝑤𝑤𝑥) → ∃𝑥𝑧(∃𝑥((𝑧𝑤𝑤𝑥) ∧ (𝑧𝑥𝑥𝑦)) ↔ 𝑧 = 𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wal 1526  wex 1771  ∃!weu 2646  wral 3135  wrex 3136  ∃!wreu 3137
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-cleq 2811  df-clel 2890  df-ral 3140  df-rex 3141  df-reu 3142
This theorem is referenced by:  aceq0  9532  dfac1  9548
  Copyright terms: Public domain W3C validator