Metamath Proof Explorer

Theorem dfac5lem4

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

Ref Expression
Hypotheses dfac5lem.1 
|- A = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) }
dfac5lem.2 
|- B = ( U. A i^i y )
dfac5lem.3 
|- ( ph <-> A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )
Assertion dfac5lem4 
|- ( ph -> E. y A. z e. A E! v v e. ( z i^i y ) )

Proof

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