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

Metamath Proof Explorer

Theorem axacnd

Description: A version of 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 axacnd ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) )

Proof

Step Hyp Ref Expression
1 axacndlem5 ⊢ ∃ 𝑥 ∀ 𝑦 ∀ 𝑣 ( ∀ 𝑥 ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) )
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 nfcvf ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 𝑦 )
15 14 3ad2ant2 ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑧 𝑦 )
16 nfcvd ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑧 𝑣 )
17 15 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 15 19 nfeld ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑧 𝑦 ∈ 𝑤 )
28 nfcvf ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 𝑥 )
29 28 3ad2ant1 ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑧 𝑥 )
30 19 29 nfeld ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑧 𝑤 ∈ 𝑥 )
31 27 30 nfand ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑧 ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) )
32 21 31 nfand ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑧 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) )
33 26 32 nfexd ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑧 ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) )
34 15 19 nfeqd ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑧 𝑦 = 𝑤 )
35 33 34 nfbid ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑧 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) )
36 9 35 nfald ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑧 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) )
37 26 36 nfexd ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑧 ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) )
38 22 37 nfimd ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
39 nfcvd ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑥 𝑣 )
40 nfcvf2 ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑥 𝑧 )
41 40 3ad2ant1 ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑥 𝑧 )
42 39 41 nfeqd ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑥 𝑣 = 𝑧 )
43 5 42 nfan1 ⊢ Ⅎ 𝑥 ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) ∧ 𝑣 = 𝑧 )
44 simpr ⊢ ( ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) ∧ 𝑣 = 𝑧 ) → 𝑣 = 𝑧 )
45 44 eleq2d ⊢ ( ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) ∧ 𝑣 = 𝑧 ) → ( 𝑦 ∈ 𝑣 ↔ 𝑦 ∈ 𝑧 ) )
46 44 eleq1d ⊢ ( ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) ∧ 𝑣 = 𝑧 ) → ( 𝑣 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤 ) )
47 45 46 anbi12d ⊢ ( ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) ∧ 𝑣 = 𝑧 ) → ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ↔ ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ) )
48 43 47 albid ⊢ ( ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) ∧ 𝑣 = 𝑧 ) → ( ∀ 𝑥 ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ↔ ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ) )
49 nfcvd ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑤 𝑣 )
50 nfcvf2 ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑤 → Ⅎ 𝑤 𝑧 )
51 50 3ad2ant3 ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑤 𝑧 )
52 49 51 nfeqd ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑤 𝑣 = 𝑧 )
53 26 52 nfan1 ⊢ Ⅎ 𝑤 ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) ∧ 𝑣 = 𝑧 )
54 nfcvd ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑦 𝑣 )
55 nfcvf2 ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑦 𝑧 )
56 55 3ad2ant2 ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑦 𝑧 )
57 54 56 nfeqd ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → Ⅎ 𝑦 𝑣 = 𝑧 )
58 9 57 nfan1 ⊢ Ⅎ 𝑦 ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) ∧ 𝑣 = 𝑧 )
59 47 anbi1d ⊢ ( ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) ∧ 𝑣 = 𝑧 ) → ( ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ) )
60 53 59 exbid ⊢ ( ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) ∧ 𝑣 = 𝑧 ) → ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ) )
61 60 bibi1d ⊢ ( ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) ∧ 𝑣 = 𝑧 ) → ( ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ↔ ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
62 58 61 albid ⊢ ( ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) ∧ 𝑣 = 𝑧 ) → ( ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ↔ ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
63 53 62 exbid ⊢ ( ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) ∧ 𝑣 = 𝑧 ) → ( ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ↔ ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
64 48 63 imbi12d ⊢ ( ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) ∧ 𝑣 = 𝑧 ) → ( ( ∀ 𝑥 ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ) )
65 64 ex ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → ( 𝑣 = 𝑧 → ( ( ∀ 𝑥 ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ) ) )
66 13 38 65 cbvald ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → ( ∀ 𝑣 ( ∀ 𝑥 ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ↔ ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ) )
67 9 66 albid ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → ( ∀ 𝑦 ∀ 𝑣 ( ∀ 𝑥 ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ↔ ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ) )
68 5 67 exbid ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → ( ∃ 𝑥 ∀ 𝑦 ∀ 𝑣 ( ∀ 𝑥 ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ) )
69 1 68 mpbii ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑥 ∧ ¬ ∀ 𝑧 𝑧 = 𝑦 ∧ ¬ ∀ 𝑧 𝑧 = 𝑤 ) → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
70 69 3exp ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( ¬ ∀ 𝑧 𝑧 = 𝑤 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) ) ) )
71 axacndlem2 ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
72 71 aecoms ⊢ ( ∀ 𝑧 𝑧 = 𝑥 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
73 axacndlem3 ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
74 73 aecoms ⊢ ( ∀ 𝑧 𝑧 = 𝑦 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
75 nfae ⊢ Ⅎ 𝑦 ∀ 𝑧 𝑧 = 𝑤
76 simpr ⊢ ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → 𝑧 ∈ 𝑤 )
77 76 alimi ⊢ ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∀ 𝑥 𝑧 ∈ 𝑤 )
78 nd3 ⊢ ( ∀ 𝑧 𝑧 = 𝑤 → ¬ ∀ 𝑥 𝑧 ∈ 𝑤 )
79 78 pm2.21d ⊢ ( ∀ 𝑧 𝑧 = 𝑤 → ( ∀ 𝑥 𝑧 ∈ 𝑤 → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
80 77 79 syl5 ⊢ ( ∀ 𝑧 𝑧 = 𝑤 → ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
81 80 axc4i ⊢ ( ∀ 𝑧 𝑧 = 𝑤 → ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
82 75 81 alrimi ⊢ ( ∀ 𝑧 𝑧 = 𝑤 → ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
83 82 19.8ad ⊢ ( ∀ 𝑧 𝑧 = 𝑤 → ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) ) )
84 70 72 74 83 pm2.61iii ⊢ ∃ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ∀ 𝑥 ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) → ∃ 𝑤 ∀ 𝑦 ( ∃ 𝑤 ( ( 𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤 ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) ) ↔ 𝑦 = 𝑤 ) )