Metamath Proof Explorer


Theorem aceq2

Description: Equivalence of two versions of the Axiom of Choice. The proof uses neither AC nor the Axiom of Regularity. (Contributed by NM, 5-Apr-2004)

Ref Expression
Assertion aceq2 ( ∃ 𝑦𝑧𝑥𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∃ 𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )

Proof

Step Hyp Ref Expression
1 df-ral ( ∀ 𝑡𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∀ 𝑡 ( 𝑡𝑧 → ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ) )
2 19.23v ( ∀ 𝑡 ( 𝑡𝑧 → ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ) ↔ ( ∃ 𝑡 𝑡𝑧 → ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ) )
3 1 2 bitri ( ∀ 𝑡𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ( ∃ 𝑡 𝑡𝑧 → ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ) )
4 biidd ( 𝑤 = 𝑡 → ( ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ) )
5 4 cbvralvw ( ∀ 𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∀ 𝑡𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) )
6 n0 ( 𝑧 ≠ ∅ ↔ ∃ 𝑡 𝑡𝑧 )
7 elequ2 ( 𝑣 = 𝑢 → ( 𝑧𝑣𝑧𝑢 ) )
8 elequ2 ( 𝑣 = 𝑢 → ( 𝑤𝑣𝑤𝑢 ) )
9 7 8 anbi12d ( 𝑣 = 𝑢 → ( ( 𝑧𝑣𝑤𝑣 ) ↔ ( 𝑧𝑢𝑤𝑢 ) ) )
10 9 cbvrexvw ( ∃ 𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ↔ ∃ 𝑢𝑦 ( 𝑧𝑢𝑤𝑢 ) )
11 10 reubii ( ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ↔ ∃! 𝑤𝑧𝑢𝑦 ( 𝑧𝑢𝑤𝑢 ) )
12 elequ1 ( 𝑤 = 𝑣 → ( 𝑤𝑢𝑣𝑢 ) )
13 12 anbi2d ( 𝑤 = 𝑣 → ( ( 𝑧𝑢𝑤𝑢 ) ↔ ( 𝑧𝑢𝑣𝑢 ) ) )
14 13 rexbidv ( 𝑤 = 𝑣 → ( ∃ 𝑢𝑦 ( 𝑧𝑢𝑤𝑢 ) ↔ ∃ 𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ) )
15 14 cbvreuvw ( ∃! 𝑤𝑧𝑢𝑦 ( 𝑧𝑢𝑤𝑢 ) ↔ ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) )
16 11 15 bitri ( ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ↔ ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) )
17 6 16 imbi12i ( ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) ↔ ( ∃ 𝑡 𝑡𝑧 → ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ) )
18 3 5 17 3bitr4i ( ∀ 𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )
19 18 ralbii ( ∀ 𝑧𝑥𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )
20 19 exbii ( ∃ 𝑦𝑧𝑥𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∃ 𝑦𝑧𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤𝑧𝑣𝑦 ( 𝑧𝑣𝑤𝑣 ) ) )