Metamath Proof Explorer


Theorem dfac5lem4

Description: Lemma for dfac5 . (Contributed by NM, 11-Apr-2004)

Ref Expression
Hypotheses dfac5lem.1 A = u | u t h u = t × t
dfac5lem.2 B = A y
dfac5lem.3 φ x z x z z x w x z w z w = y z x ∃! v v z y
Assertion dfac5lem4 φ y z A ∃! v v z y

Proof

Step Hyp Ref Expression
1 dfac5lem.1 A = u | u t h u = t × t
2 dfac5lem.2 B = A y
3 dfac5lem.3 φ x z x z z x w x z w z w = y z x ∃! v v z y
4 vex z V
5 neeq1 u = z u z
6 eqeq1 u = z u = t × t z = t × t
7 6 rexbidv u = z t h u = t × t t h z = t × t
8 5 7 anbi12d u = z u t h u = t × t z t h z = t × t
9 4 8 elab z u | u t h u = t × t z t h z = t × t
10 9 simplbi z u | u t h u = t × t z
11 10 1 eleq2s z A z
12 11 rgen z A z
13 df-an x z x w ¬ x z ¬ x w
14 4 8 1 elab2 z A z t h z = t × t
15 14 simprbi z A t h z = t × t
16 vex w V
17 neeq1 u = w u w
18 eqeq1 u = w u = t × t w = t × t
19 18 rexbidv u = w t h u = t × t t h w = t × t
20 17 19 anbi12d u = w u t h u = t × t w t h w = t × t
21 16 20 1 elab2 w A w t h w = t × t
22 21 simprbi w A t h w = t × t
23 sneq t = g t = g
24 23 xpeq1d t = g t × t = g × t
25 xpeq2 t = g g × t = g × g
26 24 25 eqtrd t = g t × t = g × g
27 26 eqeq2d t = g w = t × t w = g × g
28 27 cbvrexvw t h w = t × t g h w = g × g
29 22 28 sylib w A g h w = g × g
30 eleq2 z = t × t x z x t × t
31 elxp x t × t u v x = u v u t v t
32 excom u v x = u v u t v t v u x = u v u t v t
33 31 32 bitri x t × t v u x = u v u t v t
34 30 33 bitrdi z = t × t x z v u x = u v u t v t
35 eleq2 w = g × g x w x g × g
36 elxp x g × g u y x = u y u g y g
37 excom u y x = u y u g y g y u x = u y u g y g
38 36 37 bitri x g × g y u x = u y u g y g
39 35 38 bitrdi w = g × g x w y u x = u y u g y g
40 34 39 bi2anan9 z = t × t w = g × g x z x w v u x = u v u t v t y u x = u y u g y g
41 exdistrv v y u x = u v u t v t u x = u y u g y g v u x = u v u t v t y u x = u y u g y g
42 40 41 bitr4di z = t × t w = g × g x z x w v y u x = u v u t v t u x = u y u g y g
43 velsn u t u = t
44 opeq1 u = t u v = t v
45 44 eqeq2d u = t x = u v x = t v
46 45 biimpac x = u v u = t x = t v
47 43 46 sylan2b x = u v u t x = t v
48 47 adantrr x = u v u t v t x = t v
49 48 exlimiv u x = u v u t v t x = t v
50 velsn u g u = g
51 opeq1 u = g u y = g y
52 51 eqeq2d u = g x = u y x = g y
53 52 biimpac x = u y u = g x = g y
54 50 53 sylan2b x = u y u g x = g y
55 54 adantrr x = u y u g y g x = g y
56 55 exlimiv u x = u y u g y g x = g y
57 49 56 sylan9req u x = u v u t v t u x = u y u g y g t v = g y
58 vex t V
59 vex v V
60 58 59 opth1 t v = g y t = g
61 57 60 syl u x = u v u t v t u x = u y u g y g t = g
62 61 exlimivv v y u x = u v u t v t u x = u y u g y g t = g
63 42 62 syl6bi z = t × t w = g × g x z x w t = g
64 63 26 syl6 z = t × t w = g × g x z x w t × t = g × g
65 eqeq12 z = t × t w = g × g z = w t × t = g × g
66 64 65 sylibrd z = t × t w = g × g x z x w z = w
67 66 ex z = t × t w = g × g x z x w z = w
68 67 rexlimivw t h z = t × t w = g × g x z x w z = w
69 68 rexlimdvw t h z = t × t g h w = g × g x z x w z = w
70 69 imp t h z = t × t g h w = g × g x z x w z = w
71 15 29 70 syl2an z A w A x z x w z = w
72 13 71 syl5bir z A w A ¬ x z ¬ x w z = w
73 72 necon1ad z A w A z w x z ¬ x w
74 73 alrimdv z A w A z w x x z ¬ x w
75 disj1 z w = x x z ¬ x w
76 74 75 syl6ibr z A w A z w z w =
77 76 rgen2 z A w A z w z w =
78 vex h V
79 vuniex h V
80 78 79 xpex h × h V
81 80 pwex 𝒫 h × h V
82 snssi t h t h
83 elssuni t h t h
84 xpss12 t h t h t × t h × h
85 82 83 84 syl2anc t h t × t h × h
86 snex t V
87 86 58 xpex t × t V
88 87 elpw t × t 𝒫 h × h t × t h × h
89 85 88 sylibr t h t × t 𝒫 h × h
90 eleq1 u = t × t u 𝒫 h × h t × t 𝒫 h × h
91 89 90 syl5ibrcom t h u = t × t u 𝒫 h × h
92 91 rexlimiv t h u = t × t u 𝒫 h × h
93 92 adantl u t h u = t × t u 𝒫 h × h
94 93 abssi u | u t h u = t × t 𝒫 h × h
95 81 94 ssexi u | u t h u = t × t V
96 1 95 eqeltri A V
97 raleq x = A z x z z A z
98 raleq x = A w x z w z w = w A z w z w =
99 98 raleqbi1dv x = A z x w x z w z w = z A w A z w z w =
100 97 99 anbi12d x = A z x z z x w x z w z w = z A z z A w A z w z w =
101 raleq x = A z x ∃! v v z y z A ∃! v v z y
102 101 exbidv x = A y z x ∃! v v z y y z A ∃! v v z y
103 100 102 imbi12d x = A z x z z x w x z w z w = y z x ∃! v v z y z A z z A w A z w z w = y z A ∃! v v z y
104 96 103 spcv x z x z z x w x z w z w = y z x ∃! v v z y z A z z A w A z w z w = y z A ∃! v v z y
105 3 104 sylbi φ z A z z A w A z w z w = y z A ∃! v v z y
106 12 77 105 mp2ani φ y z A ∃! v v z y