Metamath Proof Explorer


Theorem kmlem2

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. (Contributed by NM, 25-Mar-2004)

Ref Expression
Assertion kmlem2 y z x φ ∃! w w z y y ¬ y x z x φ ∃! w w z y

Proof

Step Hyp Ref Expression
1 ineq2 y = v z y = z v
2 1 eleq2d y = v w z y w z v
3 2 eubidv y = v ∃! w w z y ∃! w w z v
4 3 imbi2d y = v φ ∃! w w z y φ ∃! w w z v
5 4 ralbidv y = v z x φ ∃! w w z y z x φ ∃! w w z v
6 5 cbvexvw y z x φ ∃! w w z y v z x φ ∃! w w z v
7 indi z v u = z v z u
8 elssuni z x z x
9 8 ssneld z x ¬ u x ¬ u z
10 disjsn z u = ¬ u z
11 9 10 syl6ibr z x ¬ u x z u =
12 11 impcom ¬ u x z x z u =
13 12 uneq2d ¬ u x z x z v z u = z v
14 un0 z v = z v
15 13 14 syl6eq ¬ u x z x z v z u = z v
16 7 15 syl5req ¬ u x z x z v = z v u
17 16 eleq2d ¬ u x z x w z v w z v u
18 17 eubidv ¬ u x z x ∃! w w z v ∃! w w z v u
19 18 imbi2d ¬ u x z x φ ∃! w w z v φ ∃! w w z v u
20 19 ralbidva ¬ u x z x φ ∃! w w z v z x φ ∃! w w z v u
21 vsnid u u
22 21 olci u v u u
23 elun u v u u v u u
24 22 23 mpbir u v u
25 elssuni v u x v u x
26 25 sseld v u x u v u u x
27 24 26 mpi v u x u x
28 27 con3i ¬ u x ¬ v u x
29 28 biantrurd ¬ u x z x φ ∃! w w z v u ¬ v u x z x φ ∃! w w z v u
30 20 29 bitrd ¬ u x z x φ ∃! w w z v ¬ v u x z x φ ∃! w w z v u
31 vex v V
32 snex u V
33 31 32 unex v u V
34 eleq1 y = v u y x v u x
35 34 notbid y = v u ¬ y x ¬ v u x
36 ineq2 y = v u z y = z v u
37 36 eleq2d y = v u w z y w z v u
38 37 eubidv y = v u ∃! w w z y ∃! w w z v u
39 38 imbi2d y = v u φ ∃! w w z y φ ∃! w w z v u
40 39 ralbidv y = v u z x φ ∃! w w z y z x φ ∃! w w z v u
41 35 40 anbi12d y = v u ¬ y x z x φ ∃! w w z y ¬ v u x z x φ ∃! w w z v u
42 33 41 spcev ¬ v u x z x φ ∃! w w z v u y ¬ y x z x φ ∃! w w z y
43 30 42 syl6bi ¬ u x z x φ ∃! w w z v y ¬ y x z x φ ∃! w w z y
44 vuniex x V
45 eleq2 y = x u y u x
46 45 notbid y = x ¬ u y ¬ u x
47 46 exbidv y = x u ¬ u y u ¬ u x
48 nalset ¬ y u u y
49 alexn y u ¬ u y ¬ y u u y
50 48 49 mpbir y u ¬ u y
51 50 spi u ¬ u y
52 44 47 51 vtocl u ¬ u x
53 43 52 exlimiiv z x φ ∃! w w z v y ¬ y x z x φ ∃! w w z y
54 53 exlimiv v z x φ ∃! w w z v y ¬ y x z x φ ∃! w w z y
55 6 54 sylbi y z x φ ∃! w w z y y ¬ y x z x φ ∃! w w z y
56 exsimpr y ¬ y x z x φ ∃! w w z y y z x φ ∃! w w z y
57 55 56 impbii y z x φ ∃! w w z y y ¬ y x z x φ ∃! w w z y