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 
|- E. x A. y A. z ( A. x ( y e. z /\ z e. w ) -> E. w A. y ( E. w ( ( y e. z /\ z e. w ) /\ ( y e. w /\ w e. x ) ) <-> y = w ) )

Proof

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