HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem axpowndlem2 4950
Description: Lemma for the Axiom of Power Sets with no distinct variable conditions.
Assertion
Ref Expression
axpowndlem2 |- (-. A.x x = y -> (-. A.x x = z -> (-. x = y -> E.xA.y(A.x(E.z x e. y -> A.y x e. z) -> y e. x))))
Distinct variable group:   y,z
Proof of Theorem axpowndlem2
StepHypRef Expression
1 axpow 2743 . . . . . . 7 |- E.wA.y(A.w(w e. y -> w e. z) -> y e. w)
2 19.8a 1029 . . . . . . . . . . . 12 |- (w e. y -> E.z w e. y)
3 ax-4 973 . . . . . . . . . . . 12 |- (A.y w e. z -> w e. z)
42, 3imim12i 18 . . . . . . . . . . 11 |- ((E.z w e. y -> A.y w e. z) -> (w e. y -> w e. z))
5419.20i 992 . . . . . . . . . 10 |- (A.w(E.z w e. y -> A.y w e. z) -> A.w(w e. y -> w e. z))
65imim1i 16 . . . . . . . . 9 |- ((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))
7619.20i 992 . . . . . . . 8 |- (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))
8719.22i 1040 . . . . . . 7 |- (E.wA.y(A.w(w e. y -> w e. z) -> y e. w) -> E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w))
91, 8ax-mp 7 . . . . . 6 |- E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w)
109a1i 8 . . . . 5 |- (-. w = y -> E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w))
1110ax-gen 963 . . . 4 |- A.w(-. w = y -> E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w))
12 hbnae 1147 . . . . . 6 |- (-. A.x x = y -> A.x -. A.x x = y)
13 hbnae 1147 . . . . . 6 |- (-. A.x x = z -> A.x -. A.x x = z)
1412, 13hban 1009 . . . . 5 |- ((-. A.x x = y /\ -. A.x x = z) -> A.x(-. A.x x = y /\ -. A.x x = z))
15 dveeq2 1212 . . . . . . . 8 |- (-. A.x x = y -> (w = y -> A.x w = y))
1612, 15hbnd 1109 . . . . . . 7 |- (-. A.x x = y -> (-. w = y -> A.x -. w = y))
1716adantr 389 . . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> (-. w = y -> A.x -. w = y))
18 ax-17 971 . . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> A.w(-. A.x x = y /\ -. A.x x = z))
19 hbnae 1147 . . . . . . . . 9 |- (-. A.x x = y -> A.y -. A.x x = y)
20 hbnae 1147 . . . . . . . . 9 |- (-. A.x x = z -> A.y -. A.x x = z)
2119, 20hban 1009 . . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> A.y(-. A.x x = y /\ -. A.x x = z))
22 hbnae 1147 . . . . . . . . . . 11 |- (-. A.x x = y -> A.w -. A.x x = y)
23 hbnae 1147 . . . . . . . . . . 11 |- (-. A.x x = z -> A.w -. A.x x = z)
2422, 23hban 1009 . . . . . . . . . 10 |- ((-. A.x x = y /\ -. A.x x = z) -> A.w(-. A.x x = y /\ -. A.x x = z))
25 hbnae 1147 . . . . . . . . . . . . 13 |- (-. A.x x = y -> A.z -. A.x x = y)
26 hbnae 1147 . . . . . . . . . . . . 13 |- (-. A.x x = z -> A.z -. A.x x = z)
2725, 26hban 1009 . . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = z) -> A.z(-. A.x x = y /\ -. A.x x = z))
28 dveel2 1357 . . . . . . . . . . . . 13 |- (-. A.x x = y -> (w e. y -> A.x w e. y))
2928adantr 389 . . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = z) -> (w e. y -> A.x w e. y))
3027, 29hbexd 1114 . . . . . . . . . . 11 |- ((-. A.x x = y /\ -. A.x x = z) -> (E.z w e. y -> A.xE.z w e. y))
31 dveel2 1357 . . . . . . . . . . . . 13 |- (-. A.x x = z -> (w e. z -> A.x w e. z))
3231adantl 388 . . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = z) -> (w e. z -> A.x w e. z))
3321, 32hbald 1113 . . . . . . . . . . 11 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.y w e. z -> A.xA.y w e. z))
3414, 30, 33hbimd 1110 . . . . . . . . . 10 |- ((-. A.x x = y /\ -. A.x x = z) -> ((E.z w e. y -> A.y w e. z) -> A.x(E.z w e. y -> A.y w e. z)))
3524, 34hbald 1113 . . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.w(E.z w e. y -> A.y w e. z) -> A.xA.w(E.z w e. y -> A.y w e. z)))
36 dveel1 1356 . . . . . . . . . 10 |- (-. A.x x = y -> (y e. w -> A.x y e. w))
3736adantr 389 . . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (y e. w -> A.x y e. w))
3814, 35, 37hbimd 1110 . . . . . . . 8 |- ((-. A.x x = y /\ -. A.x x = z) -> ((A.w(E.z w e. y -> A.y w e. z) -> y e. w) -> A.x(A.w(E.z w e. y -> A.y w e. z) -> y e. w)))
3921, 38hbald 1113 . . . . . . 7 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w) -> A.xA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w)))
4018, 39hbexd 1114 . . . . . 6 |- ((-. A.x x = y /\ -. A.x x = z) -> (E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w) -> A.xE.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w)))
4114, 17, 40hbimd 1110 . . . . 5 |- ((-. A.x x = y /\ -. A.x x = z) -> ((-. w = y -> E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w)) -> A.x(-. w = y -> E.wA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w))))
42 equequ1 1134 . . . . . . . . 9 |- (w = x -> (w = y <-> x = y))
4342negbid 611 . . . . . . . 8 |- (w = x -> (-. w = y <-> -. x = y))
4443adantl 388 . . . . . . 7 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> (-. w = y <-> -. x = y))
4518, 34hbald 1113 . . . . . . . . . . 11 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.w(E.z w e. y -> A.y w e. z) -> A.xA.w(E.z w e. y -> A.y w e. z)))
4614, 45, 37hbimd 1110 . . . . . . . . . 10 |- ((-. A.x x = y /\ -. A.x x = z) -> ((A.w(E.z w e. y -> A.y w e. z) -> y e. w) -> A.x(A.w(E.z w e. y -> A.y w e. z) -> y e. w)))
4721, 46hbald 1113 . . . . . . . . 9 |- ((-. A.x x = y /\ -. A.x x = z) -> (A.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w) -> A.xA.y(A.w(E.z w e. y -> A.y w e. z) -> y e. w)))
48 nd5 4942 . . . . . . . . . . . . 13 |- (-. A.x x = y -> (w = x -> A.y w = x))
4948adantr 389 . . . . . . . . . . . 12 |- ((-. A.x x = y /\ -. A.x x = z) -> (w = x -> A.y w = x))
5049imdistani 443 . . . . . . . . . . 11 |- (((-. A.x x = y /\ -. A.x x = z) /\ w = x) -> ((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x))
51 hba1 1003 . . . . . . . . . . . . 13 |- (A.y w = x -> A.yA.y w = x)
5221, 51hban 1009 . . . . . . . . . . . 12 |- (((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x) -> A.y((-. A.x x = y /\ -. A.x x = z) /\ A.y w = x))
53 nd5 4942 . . . . . . . . . . . . . . . . . . . 20 |- (-. A.x x = z -> (w = x -> A.z w = x))
5453imdistani 443 . . . . . . . . . . . . . . . . . . 19 |- ((-. A.x x = z /\ w = x) -> (-. A.x x = z /\ A.z w = x))
55 hba1 1003 . . . . . . . . . . . . . . . . . . . . 21 |- (A.z w = x -> A.zA.z w = x)
56 elequ1 1136 . . . . . . . . . . . . . . . . . . . . . 22 |- (w = x -> (w e. y <-> x e. y))
5756a4s 984 . . . . . . . . . . . . . . . . . . . . 21 |- (A.z w = x -> (w e. y <-> x e. y))
5855, 57exbid 1105 . . . . . . . . . . . . . . . . . . . 20 |- (A.z w = x -> (E.z w e. y <-> E.z x e. y))
5958adantl 388 . . . . . . . . . . . . . . . . . . 19 |- ((-. A.x x = z /\ A.z w = x) -> (E.z w e. y <-> E.z x e. y)