This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem aceq1

Description: Equivalence of two versions of the Axiom of Choice ax-ac . 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)

Ref Expression
Assertion aceq1 ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃ 𝑦 ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 biidd ⊢ ( 𝑤 = 𝑡 → ( ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) )
2 1 cbvralvw ⊢ ( ∀ 𝑤 ∈ ℎ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑡 ∈ ℎ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) )
3 elequ1 ⊢ ( 𝑣 = 𝑧 → ( 𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢 ) )
4 3 anbi2d ⊢ ( 𝑣 = 𝑧 → ( ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) )
5 4 rexbidv ⊢ ( 𝑣 = 𝑧 → ( ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) )
6 5 cbvreuvw ⊢ ( ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃! 𝑧 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) )
7 6 ralbii ⊢ ( ∀ 𝑡 ∈ ℎ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑡 ∈ ℎ ∃! 𝑧 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) )
8 2 7 bitri ⊢ ( ∀ 𝑤 ∈ ℎ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑡 ∈ ℎ ∃! 𝑧 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) )
9 8 ralbii ⊢ ( ∀ ℎ ∈ 𝑥 ∀ 𝑤 ∈ ℎ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ ℎ ∈ 𝑥 ∀ 𝑡 ∈ ℎ ∃! 𝑧 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) )
10 elequ1 ⊢ ( 𝑧 = ℎ → ( 𝑧 ∈ 𝑢 ↔ ℎ ∈ 𝑢 ) )
11 10 anbi1d ⊢ ( 𝑧 = ℎ → ( ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) )
12 11 rexbidv ⊢ ( 𝑧 = ℎ → ( ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) )
13 12 reueqd ⊢ ( 𝑧 = ℎ → ( ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) )
14 13 raleqbi1dv ⊢ ( 𝑧 = ℎ → ( ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑤 ∈ ℎ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ) )
15 14 cbvralvw ⊢ ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ ℎ ∈ 𝑥 ∀ 𝑤 ∈ ℎ ∃! 𝑣 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) )
16 elequ1 ⊢ ( 𝑤 = ℎ → ( 𝑤 ∈ 𝑢 ↔ ℎ ∈ 𝑢 ) )
17 16 anbi1d ⊢ ( 𝑤 = ℎ → ( ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) )
18 17 rexbidv ⊢ ( 𝑤 = ℎ → ( ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) )
19 18 reueqd ⊢ ( 𝑤 = ℎ → ( ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∃! 𝑧 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) )
20 19 raleqbi1dv ⊢ ( 𝑤 = ℎ → ( ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∀ 𝑡 ∈ ℎ ∃! 𝑧 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) )
21 20 cbvralvw ⊢ ( ∀ 𝑤 ∈ 𝑥 ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∀ ℎ ∈ 𝑥 ∀ 𝑡 ∈ ℎ ∃! 𝑧 ∈ ℎ ∃ 𝑢 ∈ 𝑦 ( ℎ ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) )
22 9 15 21 3bitr4i ⊢ ( ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑤 ∈ 𝑥 ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) )
23 22 exbii ⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃ 𝑦 ∀ 𝑤 ∈ 𝑥 ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) )
24 19.21v ⊢ ( ∀ 𝑧 ( 𝑤 ∈ 𝑥 → ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) ↔ ( 𝑤 ∈ 𝑥 → ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) )
25 impexp ⊢ ( ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑤 → ( 𝑤 ∈ 𝑥 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) )
26 bi2.04 ⊢ ( ( 𝑧 ∈ 𝑤 → ( 𝑤 ∈ 𝑥 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) ↔ ( 𝑤 ∈ 𝑥 → ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) )
27 25 26 bitri ⊢ ( ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ( 𝑤 ∈ 𝑥 → ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) )
28 27 albii ⊢ ( ∀ 𝑧 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ∀ 𝑧 ( 𝑤 ∈ 𝑥 → ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) )
29 eu6 ⊢ ( ∃! 𝑧 ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ ∃ 𝑥 ∀ 𝑧 ( ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ 𝑧 = 𝑥 ) )
30 df-reu ⊢ ( ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∃! 𝑧 ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) )
31 19.42v ⊢ ( ∃ 𝑥 ( 𝑧 ∈ 𝑤 ∧ ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) ↔ ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) )
32 an42 ⊢ ( ( ( 𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑦 ) ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ↔ ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) )
33 anass ⊢ ( ( ( 𝑧 ∈ 𝑤 ∧ 𝑥 ∈ 𝑦 ) ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑤 ∧ ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) )
34 32 33 bitr3i ⊢ ( ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝑤 ∧ ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) )
35 34 exbii ⊢ ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ ∃ 𝑥 ( 𝑧 ∈ 𝑤 ∧ ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) )
36 df-rex ⊢ ( ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∃ 𝑢 ( 𝑢 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) )
37 elequ1 ⊢ ( 𝑢 = 𝑥 → ( 𝑢 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) )
38 elequ2 ⊢ ( 𝑢 = 𝑥 → ( 𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑥 ) )
39 elequ2 ⊢ ( 𝑢 = 𝑥 → ( 𝑧 ∈ 𝑢 ↔ 𝑧 ∈ 𝑥 ) )
40 38 39 anbi12d ⊢ ( 𝑢 = 𝑥 → ( ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) )
41 37 40 anbi12d ⊢ ( 𝑢 = 𝑥 → ( ( 𝑢 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) )
42 41 cbvexvw ⊢ ( ∃ 𝑢 ( 𝑢 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) )
43 36 42 bitri ⊢ ( ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) )
44 43 anbi2i ⊢ ( ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑥 ( 𝑥 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥 ) ) ) )
45 31 35 44 3bitr4i ⊢ ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) )
46 45 bibi1i ⊢ ( ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ↔ ( ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ 𝑧 = 𝑥 ) )
47 46 albii ⊢ ( ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ↔ ∀ 𝑧 ( ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ 𝑧 = 𝑥 ) )
48 47 exbii ⊢ ( ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ↔ ∃ 𝑥 ∀ 𝑧 ( ( 𝑧 ∈ 𝑤 ∧ ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ 𝑧 = 𝑥 ) )
49 29 30 48 3bitr4i ⊢ ( ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) )
50 49 imbi2i ⊢ ( ( 𝑡 ∈ 𝑤 → ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ ( 𝑡 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )
51 50 albii ⊢ ( ∀ 𝑡 ( 𝑡 ∈ 𝑤 → ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )
52 df-ral ⊢ ( ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑤 → ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) )
53 nfv ⊢ Ⅎ 𝑡 ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) )
54 nfv ⊢ Ⅎ 𝑧 𝑡 ∈ 𝑤
55 nfa1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 )
56 55 nfex ⊢ Ⅎ 𝑧 ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 )
57 54 56 nfim ⊢ Ⅎ 𝑧 ( 𝑡 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) )
58 elequ1 ⊢ ( 𝑧 = 𝑡 → ( 𝑧 ∈ 𝑤 ↔ 𝑡 ∈ 𝑤 ) )
59 58 imbi1d ⊢ ( 𝑧 = 𝑡 → ( ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ( 𝑡 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) )
60 53 57 59 cbvalv1 ⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ∀ 𝑡 ( 𝑡 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )
61 51 52 60 3bitr4i ⊢ ( ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )
62 61 imbi2i ⊢ ( ( 𝑤 ∈ 𝑥 → ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) ↔ ( 𝑤 ∈ 𝑥 → ∀ 𝑧 ( 𝑧 ∈ 𝑤 → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) )
63 24 28 62 3bitr4i ⊢ ( ∀ 𝑧 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ( 𝑤 ∈ 𝑥 → ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) )
64 63 albii ⊢ ( ∀ 𝑤 ∀ 𝑧 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) )
65 alcom ⊢ ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ∀ 𝑤 ∀ 𝑧 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )
66 df-ral ⊢ ( ∀ 𝑤 ∈ 𝑥 ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ) )
67 64 65 66 3bitr4ri ⊢ ( ∀ 𝑤 ∈ 𝑥 ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )
68 67 exbii ⊢ ( ∃ 𝑦 ∀ 𝑤 ∈ 𝑥 ∀ 𝑡 ∈ 𝑤 ∃! 𝑧 ∈ 𝑤 ∃ 𝑢 ∈ 𝑦 ( 𝑤 ∈ 𝑢 ∧ 𝑧 ∈ 𝑢 ) ↔ ∃ 𝑦 ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )
69 23 68 bitri ⊢ ( ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ∀ 𝑤 ∈ 𝑧 ∃! 𝑣 ∈ 𝑧 ∃ 𝑢 ∈ 𝑦 ( 𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢 ) ↔ ∃ 𝑦 ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑥 ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )