HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem kmlem2 3581
Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4.
Assertion
Ref Expression
kmlem2 |- (E.yA.z e. x (ph -> E!v v e. (z i^i y)) <-> E.y(-. y e. x /\ A.z e. x (ph -> E!v v e. (z i^i y))))
Distinct variable group(s):   x,y,z,v   ph,y
Proof of Theorem kmlem2
StepHypRef Expression
1 ineq2 1639 . . . . . . . 8 |- (y = w -> (z i^i y) = (z i^i w))
21eleq2d 1156 . . . . . . 7 |- (y = w -> (v e. (z i^i y) <-> v e. (z i^i w)))
32bieudv 1013 . . . . . 6 |- (y = w -> (E!v v e. (z i^i y) <-> E!v v e. (z i^i w)))
43imbi2d 464 . . . . 5 |- (y = w -> ((ph -> E!v v e. (z i^i y)) <-> (ph -> E!v v e. (z i^i w))))
54biraldv 1219 . . . 4 |- (y = w -> (A.z e. x (ph -> E!v v e. (z i^i y)) <-> A.z e. x (ph -> E!v v e. (z i^i w))))
65cbvexv 973 . . 3 |- (E.yA.z e. x (ph -> E!v v e. (z i^i y)) <-> E.wA.z e. x (ph -> E!v v e. (z i^i w)))
7 visset 1350 . . . . . . 7 |- x e. V
87uniex 1947 . . . . . 6 |- U.x e. V
9 eleq2 1150 . . . . . . . 8 |- (y = U.x -> (u e. y <-> u e. U.x))
109negbid 463 . . . . . . 7 |- (y = U.x -> (-. u e. y <-> -. u e. U.x))
1110biexdv 936 . . . . . 6 |- (y = U.x -> (E.u -. u e. y <-> E.u -. u e. U.x))
12 nalset 1482 . . . . . . . 8 |- -. E.yA.u u e. y
13 alexn 726 . . . . . . . 8 |- (A.yE.u -. u e. y <-> -. E.yA.u u e. y)
1412, 13mpbir 165 . . . . . . 7 |- A.yE.u -. u e. y
1514a4i 680 . . . . . 6 |- E.u -. u e. y
168, 11, 15vtocl 1378 . . . . 5 |- E.u -. u e. U.x
17 elssuni 1940 . . . . . . . . . . . . . . . . . . . 20 |- (z e. x -> z (_ U.x)
1817sseld 1506 . . . . . . . . . . . . . . . . . . 19 |- (z e. x -> (u e. z -> u e. U.x))
1918con3d 87 . . . . . . . . . . . . . . . . . 18 |- (z e. x -> (-. u e. U.x -> -. u e. z))
20 disjsn 1836 . . . . . . . . . . . . . . . . . 18 |- ((z i^i {u}) = (/) <-> -. u e. z)
2119, 20syl6ibr 186 . . . . . . . . . . . . . . . . 17 |- (z e. x -> (-. u e. U.x -> (z i^i {u}) = (/)))
2221com12 13 . . . . . . . . . . . . . . . 16 |- (-. u e. U.x -> (z e. x -> (z i^i {u}) = (/)))
2322imp 277 . . . . . . . . . . . . . . 15 |- ((-. u e. U.x /\ z e. x) -> (z i^i {u}) = (/))
2423uneq2d 1611 . . . . . . . . . . . . . 14 |- ((-. u e. U.x /\ z e. x) -> ((z i^i w) u. (z i^i {u})) = ((z i^i w) u. (/)))
25 un0 1721 . . . . . . . . . . . . . 14 |- ((z i^i w) u. (/)) = (z i^i w)
2624, 25syl6eq 1140 . . . . . . . . . . . . 13 |- ((-. u e. U.x /\ z e. x) -> ((z i^i w) u. (z i^i {u})) = (z i^i w))
27 indi 1676 . . . . . . . . . . . . 13 |- (z i^i (w u. {u})) = ((z i^i w) u. (z i^i {u}))
2826, 27syl5req 1137 . . . . . . . . . . . 12 |- ((-. u e. U.x /\ z e. x) -> (z i^i w) = (z i^i (w u. {u})))
2928eleq2d 1156 . . . . . . . . . . 11 |- ((-. u e. U.x /\ z e. x) -> (v e. (z i^i w) <-> v e. (z i^i (w u. {u}))))
3029bieudv 1013 . . . . . . . . . 10 |- ((-. u e. U.x /\ z e. x) -> (E!v v e. (z i^i w) <-> E!v v e. (z i^i (w u. {u}))))
3130imbi2d 464 . . . . . . . . 9 |- ((-. u e. U.x /\ z e. x) -> ((ph -> E!v v e. (z i^i w)) <-> (ph -> E!v v e. (z i^i (w u. {u})))))
3231biraldva 1215 . . . . . . . 8 |- (-. u e. U.x -> (A.z e. x (ph -> E!v v e. (z i^i w)) <-> A.z e. x (ph -> E!v v e. (z i^i (w u. {u})))))
33 visset 1350 . . . . . . . . . . . . . . 15 |- u e. V
3433snid 1830 . . . . . . . . . . . . . 14 |- u e. {u}
3534a1i 7 . . . . . . . . . . . . 13 |- (-. u e. w -> u e. {u})
3635orri 201 . . . . . . . . . . . 12 |- (u e. w \/ u e. {u})
37 elun 1601 . . . . . . . . . . . 12 |- (u e. (w u. {u}) <-> (u e. w \/ u e. {u}))
3836, 37mpbir 165 . . . . . . . . . . 11 |- u e. (w u. {u})
39 elssuni 1940 . . . . . . . . . . . 12 |- ((w u. {u}) e. x -> (w u. {u}) (_ U.x)
4039sseld 1506 . . . . . . . . . . 11 |- ((w u. {u}) e. x -> (u e. (w u. {u}) -> u e. U.x))
4138, 40mpi 44 . . . . . . . . . 10 |- ((w u. {u}) e. x -> u e. U.x)
4241con3i 90 . . . . . . . . 9 |- (-. u e. U.x -> -. (w u. {u}) e. x)
4342biantrurd 546 . . . . . . . 8 |- (-. u e. U.x -> (A.z e. x (ph -> E!v v e. (z i^i (w u. {u}))) <-> (-. (w u. {u}) e. x /\ A.z e. x (ph -> E!v v e. (z i^i (w u. {u}))))))
4432, 43bitrd 406 . . . . . . 7 |- (-. u e. U.x -> (A.z e. x (ph -> E!v v e. (z i^i w)) <-> (-. (w u. {u}) e. x /\ A.z e. x (ph -> E!v v e. (z i^i (w u. {u}))))))
45 visset 1350 . . . . . . . . 9 |- w e. V
46 snex 1859 . . . . . . . . 9 |- {u} e. V
4745, 46unex 1949 . . . . . . . 8 |- (w u. {u}) e. V
48 eleq1 1149 . . . . . . . . . 10 |- (y = (w u. {u}) -> (y e. x <-> (w u. {u}) e. x))
4948negbid 463 . . . . . . . . 9 |- (y = (w u. {u}) -> (-. y e. x <-> -. (w u. {u}) e. x))
50 ineq2 1639 . . . . . . . . . . . . 13 |- (y = (w u. {u}) -> (z i^i y) = (z i^i (w u. {u})))
5150eleq2d 1156 . . . . . . . . . . . 12 |- (y = (w u. {u}) -> (v e. (z i^i y) <-> v e. (z i^i (w u. {u}))))
5251bieudv 1013 . . . . . . . . . . 11 |- (y = (w u. {u}) -> (E!v v e. (z i^i y) <-> E!v v e. (z i^i (w u. {u}))))
5352imbi2d 464 . . . . . . . . . 10 |- (y = (w u. {u}) -> ((ph -> E!v v e. (z i^i y)) <-> (ph -> E!v v e. (z i^i (w u. {u})))))
5453biraldv 1219 . . . . . . . . 9 |- (y = (w u. {u}) -> (A.z e. x (ph -> E!v v e. (z i^i y)) <-> A.z e. x (ph -> E!v v e. (z i^i (w u. {u})))))
5549, 54anbi12d 476 . . . . . . . 8 |- (y = (w u. {u}) -> ((-. y e. x /\ A.z e. x (ph -> E!v v e. (z i^i y))) <-> (-. (w u. {u}) e. x /\ A.z e. x (ph -> E!v v e. (z i^i (w u. {u}))))))
5647, 55cla4ev 1401 . . . . . . 7 |- ((-. (w u. {u}) e. x /\ A.z e. x (ph -> E!v v e. (z i^i (w u. {u})))) -> E.y(-. y e. x /\ A.z e. x (ph -> E!v v e. (z i^i y))))
5744, 56syl6bi 187 . . . . . 6 |- (-. u e. U.x -> (A.z e. x (ph -> E!v v e. (z i^i w)) -> E.y(-. y e. x /\ A.z e. x (ph -> E!v v e. (z i^i y)))))
585719.23aiv 952 . . . . 5 |- (E.u -. u e. U.x -> (A.z e. x (ph -> E!v v e. (z i^i w)) -> E.y(-. y e. x /\ A.z e. x (ph -> E!v v e. (z i^i y)))))
5916, 58ax-mp 6 . . . 4 |- (A.z e. x (ph -> E!v v e. (z i^i w)) -> E.y(-. y e. x /\ A.z e. x (ph -> E!v v e. (z i^i y))))
605919.23aiv 952 . . 3 |- (E.wA.z e. x (ph -> E!v v e. (z i^i w)) -> E.y(-. y e. x /\ A.z e. x (ph -> E!v v e. (z i^i y))))
616, 60sylbi 174 . 2 |- (E.yA.z e. x (ph -> E!v v e. (z i^i y)) -> E.y(-. y e. x /\ A.z e. x (ph -> E!v v e. (z i^i y))))
62 pm3.27 260 . . 3 |- ((-. y e. x /\ A.z e. x (ph -> E!v v e. (z i^i y))) -> A.z e. x (ph -> E!v v e. (z i^i y)))
636219.22i 723 . 2 |- (E.y(-. y e. x /\ A.z e. x (ph -> E!v v e. (z i^i y))) -> E.yA.z e. x (ph -> E!v v e. (z i^i y)))
6461, 63impbi 139 1 |- (E.yA.z e. x (ph -> E!v v e. (z i^i y)) <-> E.y(-. y e. x /\ A.z e. x (ph -> E!v v e. (z i^i y))))
Colors of variables: wff set class
Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   \/ wo 195   /\ wa 196  A.wal 672  E.wex 678   = weq 797   e. wel 803  E!weu 1007   = wceq 1091   e. wcel 1092  A.wral 1201   u. cun 1485   i^i cin 1486  (/)c0 1707  {csn 1808  U.cuni 1919
This theorem is referenced by:  kmlem13 3592
This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077
This theorem depends on definitions:  df-bi