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 𝑥𝑦𝑧 ( ∀ 𝑥 ( 𝑦𝑧𝑧𝑤 ) → ∃ 𝑤𝑦 ( ∃ 𝑤 ( ( 𝑦𝑧𝑧𝑤 ) ∧ ( 𝑦𝑤𝑤𝑥 ) ) ↔ 𝑦 = 𝑤 ) )