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

Metamath Proof Explorer

Theorem axpowndlem2

Description: Lemma for the Axiom of Power Sets with no distinct variable conditions. Revised to remove a redundant antecedent from the consequence. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 4-Jan-2002) (Proof shortened by Mario Carneiro, 6-Dec-2016) (Revised and shortened by Wolf Lammen, 9-Jun-2019.) (New usage is discouraged.)

Ref Expression
Assertion axpowndlem2 
|- ( -. A. x x = y -> ( -. A. x x = z -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )

Proof

Step Hyp Ref Expression
1 zfpow 
 |-  E. w A. y ( A. w ( w e. y -> w e. z ) -> y e. w )
2 19.8a 
 |-  ( w e. y -> E. z w e. y )
3 sp 
 |-  ( A. y w e. z -> w e. z )
4 2 3 imim12i 
 |-  ( ( E. z w e. y -> A. y w e. z ) -> ( w e. y -> w e. z ) )
5 4 alimi 
 |-  ( A. w ( E. z w e. y -> A. y w e. z ) -> A. w ( w e. y -> w e. z ) )
6 5 imim1i 
 |-  ( ( A. w ( w e. y -> w e. z ) -> y e. w ) -> ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) )
7 6 alimi 
 |-  ( A. y ( A. w ( w e. y -> w e. z ) -> y e. w ) -> A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) )
8 1 7 eximii 
 |-  E. w A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w )
9 nfnae 
 |-  F/ x -. A. x x = y
10 nfnae 
 |-  F/ x -. A. x x = z
11 9 10 nfan 
 |-  F/ x ( -. A. x x = y /\ -. A. x x = z )
12 nfnae 
 |-  F/ y -. A. x x = y
13 nfnae 
 |-  F/ y -. A. x x = z
14 12 13 nfan 
 |-  F/ y ( -. A. x x = y /\ -. A. x x = z )
15 nfv 
 |-  F/ w ( -. A. x x = y /\ -. A. x x = z )
16 nfnae 
 |-  F/ z -. A. x x = y
17 nfcvd 
 |-  ( -. A. x x = y -> F/_ x w )
18 nfcvf 
 |-  ( -. A. x x = y -> F/_ x y )
19 17 18 nfeld 
 |-  ( -. A. x x = y -> F/ x w e. y )
20 16 19 nfexd 
 |-  ( -. A. x x = y -> F/ x E. z w e. y )
21 20 adantr 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x E. z w e. y )
22 nfcvd 
 |-  ( -. A. x x = z -> F/_ x w )
23 nfcvf 
 |-  ( -. A. x x = z -> F/_ x z )
24 22 23 nfeld 
 |-  ( -. A. x x = z -> F/ x w e. z )
25 13 24 nfald 
 |-  ( -. A. x x = z -> F/ x A. y w e. z )
26 25 adantl 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. y w e. z )
27 21 26 nfimd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( E. z w e. y -> A. y w e. z ) )
28 15 27 nfald 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. w ( E. z w e. y -> A. y w e. z ) )
29 18 17 nfeld 
 |-  ( -. A. x x = y -> F/ x y e. w )
30 29 adantr 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x y e. w )
31 28 30 nfimd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) )
32 14 31 nfald 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) )
33 nfeqf2 
 |-  ( -. A. y y = x -> F/ y w = x )
34 33 naecoms 
 |-  ( -. A. x x = y -> F/ y w = x )
35 34 adantr 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ y w = x )
36 14 35 nfan1 
 |-  F/ y ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x )
37 nfnae 
 |-  F/ z -. A. x x = z
38 nfeqf2 
 |-  ( -. A. z z = x -> F/ z w = x )
39 38 naecoms 
 |-  ( -. A. x x = z -> F/ z w = x )
40 37 39 nfan1 
 |-  F/ z ( -. A. x x = z /\ w = x )
41 elequ1 
 |-  ( w = x -> ( w e. y <-> x e. y ) )
42 41 adantl 
 |-  ( ( -. A. x x = z /\ w = x ) -> ( w e. y <-> x e. y ) )
43 40 42 exbid 
 |-  ( ( -. A. x x = z /\ w = x ) -> ( E. z w e. y <-> E. z x e. y ) )
44 43 adantll 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( E. z w e. y <-> E. z x e. y ) )
45 12 34 nfan1 
 |-  F/ y ( -. A. x x = y /\ w = x )
46 elequ1 
 |-  ( w = x -> ( w e. z <-> x e. z ) )
47 46 adantl 
 |-  ( ( -. A. x x = y /\ w = x ) -> ( w e. z <-> x e. z ) )
48 45 47 albid 
 |-  ( ( -. A. x x = y /\ w = x ) -> ( A. y w e. z <-> A. y x e. z ) )
49 48 adantlr 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. y w e. z <-> A. y x e. z ) )
50 44 49 imbi12d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( E. z w e. y -> A. y w e. z ) <-> ( E. z x e. y -> A. y x e. z ) ) )
51 50 ex 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( ( E. z w e. y -> A. y w e. z ) <-> ( E. z x e. y -> A. y x e. z ) ) ) )
52 11 27 51 cbvald 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( A. w ( E. z w e. y -> A. y w e. z ) <-> A. x ( E. z x e. y -> A. y x e. z ) ) )
53 52 adantr 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. w ( E. z w e. y -> A. y w e. z ) <-> A. x ( E. z x e. y -> A. y x e. z ) ) )
54 elequ2 
 |-  ( w = x -> ( y e. w <-> y e. x ) )
55 54 adantl 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( y e. w <-> y e. x ) )
56 53 55 imbi12d 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) <-> ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
57 36 56 albid 
 |-  ( ( ( -. A. x x = y /\ -. A. x x = z ) /\ w = x ) -> ( A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) <-> A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
58 57 ex 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( w = x -> ( A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) <-> A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) ) )
59 11 32 58 cbvexd 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( E. w A. y ( A. w ( E. z w e. y -> A. y w e. z ) -> y e. w ) <-> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )
60 8 59 mpbii 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) )
61 60 ex 
 |-  ( -. A. x x = y -> ( -. A. x x = z -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) ) )