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

Metamath Proof Explorer

Theorem axacndlem5

Description: Lemma for the Axiom of Choice with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 3-Jan-2002) (Proof shortened by Mario Carneiro, 10-Dec-2016)

Ref Expression
Assertion axacndlem5 ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) )

Proof

Step Hyp Ref Expression
1 axacndlem4 ⊢ ∃ 𝑥 ∀ 𝑣 ∀ 𝑧 ( ∀ 𝑥 ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑣 ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) )
2 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑧
3 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑥
4 nfnae ⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑤
5 2 3 4 nf3an ⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 )
6 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑦 𝑦 = 𝑧
7 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑦 𝑦 = 𝑥
8 nfnae ⊢ Ⅎ 𝑦 ¬ ∀ 𝑦 𝑦 = 𝑤
9 6 7 8 nf3an ⊢ Ⅎ 𝑦 ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 )
10 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑦 𝑦 = 𝑧
11 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑦 𝑦 = 𝑥
12 nfnae ⊢ Ⅎ 𝑧 ¬ ∀ 𝑦 𝑦 = 𝑤
13 10 11 12 nf3an ⊢ Ⅎ 𝑧 ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 )
14 nfcvd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 𝑣 )
15 nfcvf ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑦 𝑧 )
16 15 3ad2ant1 ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 𝑧 )
17 14 16 nfeld ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 𝑣 ∈ 𝑧 )
18 nfcvf ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑤 → Ⅎ 𝑦 𝑤 )
19 18 3ad2ant3 ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 𝑤 )
20 16 19 nfeld ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 𝑧 ∈ 𝑤 )
21 17 20 nfand ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) )
22 5 21 nfald ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 ∀ 𝑥 ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) )
23 nfnae ⊢ Ⅎ 𝑤 ¬ ∀ 𝑦 𝑦 = 𝑧
24 nfnae ⊢ Ⅎ 𝑤 ¬ ∀ 𝑦 𝑦 = 𝑥
25 nfnae ⊢ Ⅎ 𝑤 ¬ ∀ 𝑦 𝑦 = 𝑤
26 23 24 25 nf3an ⊢ Ⅎ 𝑤 ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 )
27 nfv ⊢ Ⅎ 𝑣 ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 )
28 14 19 nfeld ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 𝑣 ∈ 𝑤 )
29 nfcvf ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 𝑥 )
30 29 3ad2ant2 ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 𝑥 )
31 19 30 nfeld ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 𝑤 ∈ 𝑥 )
32 28 31 nfand ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) )
33 21 32 nfand ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) )
34 26 33 nfexd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) )
35 14 19 nfeqd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 𝑣 = 𝑤 )
36 34 35 nfbid ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) )
37 27 36 nfald ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 ∀ 𝑣 ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) )
38 26 37 nfexd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 ∃ 𝑤 ∀ 𝑣 ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) )
39 22 38 nfimd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 ( ∀ 𝑥 ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑣 ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) ) )
40 13 39 nfald ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑣 ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) ) )
41 nfcvd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑧 𝑣 )
42 nfcvf2 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 𝑦 )
43 42 3ad2ant1 ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑧 𝑦 )
44 41 43 nfeqd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑧 𝑣 = 𝑦 )
45 13 44 nfan1 ⊢ Ⅎ 𝑧 ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 )
46 nfcvd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑥 𝑣 )
47 nfcvf2 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑥 𝑦 )
48 47 3ad2ant2 ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑥 𝑦 )
49 46 48 nfeqd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑥 𝑣 = 𝑦 )
50 5 49 nfan1 ⊢ Ⅎ 𝑥 ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 )
51 simpr ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 ) → 𝑣 = 𝑦 )
52 51 eleq1d ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 ) → ( 𝑣 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) )
53 52 anbi1d ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 ) → ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ↔ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ) )
54 50 53 albid ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 ) → ( ∀ 𝑥 ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ↔ ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ) )
55 nfcvd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑤 𝑣 )
56 nfcvf2 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑤 → Ⅎ 𝑤 𝑦 )
57 56 3ad2ant3 ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑤 𝑦 )
58 55 57 nfeqd ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → Ⅎ 𝑤 𝑣 = 𝑦 )
59 26 58 nfan1 ⊢ Ⅎ 𝑤 ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 )
60 51 eleq1d ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 ) → ( 𝑣 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤 ) )
61 60 anbi1d ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 ) → ( ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ↔ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) )
62 53 61 anbi12d ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 ) → ( ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ) )
63 59 62 exbid ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 ) → ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ) )
64 51 eqeq1d ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 ) → ( 𝑣 = 𝑤 ↔ 𝑦 = 𝑤 ) )
65 63 64 bibi12d ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 ) → ( ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) ↔ ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
66 65 ex ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → ( 𝑣 = 𝑦 → ( ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) ↔ ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ) )
67 9 36 66 cbvald ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → ( ∀ 𝑣 ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) ↔ ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
68 26 67 exbid ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → ( ∃ 𝑤 ∀ 𝑣 ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) ↔ ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
69 68 adantr ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 ) → ( ∃ 𝑤 ∀ 𝑣 ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) ↔ ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
70 54 69 imbi12d ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 ) → ( ( ∀ 𝑥 ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑣 ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) ) ↔ ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ) )
71 45 70 albid ⊢ ( ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) ∧ 𝑣 = 𝑦 ) → ( ∀ 𝑧 ( ∀ 𝑥 ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑣 ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) ) ↔ ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ) )
72 71 ex ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → ( 𝑣 = 𝑦 → ( ∀ 𝑧 ( ∀ 𝑥 ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑣 ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) ) ↔ ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ) ) )
73 9 40 72 cbvald ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → ( ∀ 𝑣 ∀ 𝑧 ( ∀ 𝑥 ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑣 ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) ) ↔ ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ) )
74 5 73 exbid ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → ( ∃ 𝑥 ∀ 𝑣 ∀ 𝑧 ( ∀ 𝑥 ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑣 ( ∃ 𝑤 ( ( 𝑣 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑣 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑣 = 𝑤 ) ) ↔ ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ) )
75 1 74 mpbii ⊢ ( ( ¬ ∀ 𝑦 𝑦 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑥 ∧ ¬ ∀ 𝑦 𝑦 = 𝑤 ) → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
76 75 3exp ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ¬ ∀ 𝑦 𝑦 = 𝑤 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ) ) )
77 axacndlem3 ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
78 axacndlem1 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
79 78 aecoms ⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
80 nfae ⊢ Ⅎ 𝑧 ∀ 𝑦 𝑦 = 𝑤
81 en2lp ⊢ ¬ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑦 )
82 elequ2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑤 ) )
83 82 anbi2d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑦 ) ↔ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ) )
84 81 83 mtbii ⊢ ( 𝑦 = 𝑤 → ¬ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) )
85 84 sps ⊢ ( ∀ 𝑦 𝑦 = 𝑤 → ¬ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) )
86 85 pm2.21d ⊢ ( ∀ 𝑦 𝑦 = 𝑤 → ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
87 86 spsd ⊢ ( ∀ 𝑦 𝑦 = 𝑤 → ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
88 80 87 alrimi ⊢ ( ∀ 𝑦 𝑦 = 𝑤 → ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
89 88 axc4i ⊢ ( ∀ 𝑦 𝑦 = 𝑤 → ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
90 89 19.8ad ⊢ ( ∀ 𝑦 𝑦 = 𝑤 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
91 76 77 79 90 pm2.61iii ⊢ ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) )