Metamath Proof Explorer

Theorem dfac5lem4

Description: Lemma for dfac5 . (Contributed by NM, 11-Apr-2004) Avoid ax-11 . (Revised by BTernaryTau, 23-Jun-2025)

Ref Expression
Hypotheses dfac5lem.1 
|- A = { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) }
dfac5lem.2 
|- ( 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 
 |-  ( 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 ) ) )
3 vex 
 |-  z e. _V
4 neeq1 
 |-  ( u = z -> ( u =/= (/) <-> z =/= (/) ) )
5 eqeq1 
 |-  ( u = z -> ( u = ( { t } X. t ) <-> z = ( { t } X. t ) ) )
6 5 rexbidv 
 |-  ( u = z -> ( E. t e. h u = ( { t } X. t ) <-> E. t e. h z = ( { t } X. t ) ) )
7 4 6 anbi12d 
 |-  ( u = z -> ( ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) <-> ( z =/= (/) /\ E. t e. h z = ( { t } X. t ) ) ) )
8 3 7 elab 
 |-  ( z e. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } <-> ( z =/= (/) /\ E. t e. h z = ( { t } X. t ) ) )
9 8 simplbi 
 |-  ( z e. { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } -> z =/= (/) )
10 9 1 eleq2s 
 |-  ( z e. A -> z =/= (/) )
11 10 rgen 
 |-  A. z e. A z =/= (/)
12 df-an 
 |-  ( ( x e. z /\ x e. w ) <-> -. ( x e. z -> -. x e. w ) )
13 3 7 1 elab2 
 |-  ( z e. A <-> ( z =/= (/) /\ E. t e. h z = ( { t } X. t ) ) )
14 13 simprbi 
 |-  ( z e. A -> E. t e. h z = ( { t } X. t ) )
15 vex 
 |-  w e. _V
16 neeq1 
 |-  ( u = w -> ( u =/= (/) <-> w =/= (/) ) )
17 eqeq1 
 |-  ( u = w -> ( u = ( { t } X. t ) <-> w = ( { t } X. t ) ) )
18 17 rexbidv 
 |-  ( u = w -> ( E. t e. h u = ( { t } X. t ) <-> E. t e. h w = ( { t } X. t ) ) )
19 16 18 anbi12d 
 |-  ( u = w -> ( ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) <-> ( w =/= (/) /\ E. t e. h w = ( { t } X. t ) ) ) )
20 15 19 1 elab2 
 |-  ( w e. A <-> ( w =/= (/) /\ E. t e. h w = ( { t } X. t ) ) )
21 20 simprbi 
 |-  ( w e. A -> E. t e. h w = ( { t } X. t ) )
22 sneq 
 |-  ( t = g -> { t } = { g } )
23 22 xpeq1d 
 |-  ( t = g -> ( { t } X. t ) = ( { g } X. t ) )
24 xpeq2 
 |-  ( t = g -> ( { g } X. t ) = ( { g } X. g ) )
25 23 24 eqtrd 
 |-  ( t = g -> ( { t } X. t ) = ( { g } X. g ) )
26 25 eqeq2d 
 |-  ( t = g -> ( w = ( { t } X. t ) <-> w = ( { g } X. g ) ) )
27 26 cbvrexvw 
 |-  ( E. t e. h w = ( { t } X. t ) <-> E. g e. h w = ( { g } X. g ) )
28 21 27 sylib 
 |-  ( w e. A -> E. g e. h w = ( { g } X. g ) )
29 eleq2 
 |-  ( z = ( { t } X. t ) -> ( x e. z <-> x e. ( { t } X. t ) ) )
30 elxp 
 |-  ( x e. ( { t } X. t ) <-> E. u E. v ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) )
31 opeq1 
 |-  ( u = s -> <. u , v >. = <. s , v >. )
32 31 eqeq2d 
 |-  ( u = s -> ( x = <. u , v >. <-> x = <. s , v >. ) )
33 eleq1w 
 |-  ( u = s -> ( u e. { t } <-> s e. { t } ) )
34 33 anbi1d 
 |-  ( u = s -> ( ( u e. { t } /\ v e. t ) <-> ( s e. { t } /\ v e. t ) ) )
35 32 34 anbi12d 
 |-  ( u = s -> ( ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) <-> ( x = <. s , v >. /\ ( s e. { t } /\ v e. t ) ) ) )
36 35 excomimw 
 |-  ( 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 ) ) )
37 30 36 sylbi 
 |-  ( x e. ( { t } X. t ) -> E. v E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) )
38 29 37 biimtrdi 
 |-  ( z = ( { t } X. t ) -> ( x e. z -> E. v E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) ) )
39 eleq2 
 |-  ( w = ( { g } X. g ) -> ( x e. w <-> x e. ( { g } X. g ) ) )
40 elxp 
 |-  ( x e. ( { g } X. g ) <-> E. u E. y ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) )
41 opeq1 
 |-  ( u = s -> <. u , y >. = <. s , y >. )
42 41 eqeq2d 
 |-  ( u = s -> ( x = <. u , y >. <-> x = <. s , y >. ) )
43 eleq1w 
 |-  ( u = s -> ( u e. { g } <-> s e. { g } ) )
44 43 anbi1d 
 |-  ( u = s -> ( ( u e. { g } /\ y e. g ) <-> ( s e. { g } /\ y e. g ) ) )
45 42 44 anbi12d 
 |-  ( u = s -> ( ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) <-> ( x = <. s , y >. /\ ( s e. { g } /\ y e. g ) ) ) )
46 45 excomimw 
 |-  ( 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 ) ) )
47 40 46 sylbi 
 |-  ( x e. ( { g } X. g ) -> E. y E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) )
48 39 47 biimtrdi 
 |-  ( w = ( { g } X. g ) -> ( x e. w -> E. y E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) ) )
49 38 48 im2anan9 
 |-  ( ( 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 ) ) ) ) )
50 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 ) ) ) )
51 49 50 imbitrrdi 
 |-  ( ( 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 ) ) ) ) )
52 velsn 
 |-  ( u e. { t } <-> u = t )
53 opeq1 
 |-  ( u = t -> <. u , v >. = <. t , v >. )
54 53 eqeq2d 
 |-  ( u = t -> ( x = <. u , v >. <-> x = <. t , v >. ) )
55 54 biimpac 
 |-  ( ( x = <. u , v >. /\ u = t ) -> x = <. t , v >. )
56 52 55 sylan2b 
 |-  ( ( x = <. u , v >. /\ u e. { t } ) -> x = <. t , v >. )
57 56 adantrr 
 |-  ( ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) -> x = <. t , v >. )
58 57 exlimiv 
 |-  ( E. u ( x = <. u , v >. /\ ( u e. { t } /\ v e. t ) ) -> x = <. t , v >. )
59 velsn 
 |-  ( u e. { g } <-> u = g )
60 opeq1 
 |-  ( u = g -> <. u , y >. = <. g , y >. )
61 60 eqeq2d 
 |-  ( u = g -> ( x = <. u , y >. <-> x = <. g , y >. ) )
62 61 biimpac 
 |-  ( ( x = <. u , y >. /\ u = g ) -> x = <. g , y >. )
63 59 62 sylan2b 
 |-  ( ( x = <. u , y >. /\ u e. { g } ) -> x = <. g , y >. )
64 63 adantrr 
 |-  ( ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) -> x = <. g , y >. )
65 64 exlimiv 
 |-  ( E. u ( x = <. u , y >. /\ ( u e. { g } /\ y e. g ) ) -> x = <. g , y >. )
66 58 65 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 >. )
67 vex 
 |-  t e. _V
68 vex 
 |-  v e. _V
69 67 68 opth1 
 |-  ( <. t , v >. = <. g , y >. -> t = g )
70 66 69 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 )
71 70 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 )
72 51 71 syl6 
 |-  ( ( z = ( { t } X. t ) /\ w = ( { g } X. g ) ) -> ( ( x e. z /\ x e. w ) -> t = g ) )
73 72 25 syl6 
 |-  ( ( z = ( { t } X. t ) /\ w = ( { g } X. g ) ) -> ( ( x e. z /\ x e. w ) -> ( { t } X. t ) = ( { g } X. g ) ) )
74 eqeq12 
 |-  ( ( z = ( { t } X. t ) /\ w = ( { g } X. g ) ) -> ( z = w <-> ( { t } X. t ) = ( { g } X. g ) ) )
75 73 74 sylibrd 
 |-  ( ( z = ( { t } X. t ) /\ w = ( { g } X. g ) ) -> ( ( x e. z /\ x e. w ) -> z = w ) )
76 75 ex 
 |-  ( z = ( { t } X. t ) -> ( w = ( { g } X. g ) -> ( ( x e. z /\ x e. w ) -> z = w ) ) )
77 76 rexlimivw 
 |-  ( E. t e. h z = ( { t } X. t ) -> ( w = ( { g } X. g ) -> ( ( x e. z /\ x e. w ) -> z = w ) ) )
78 77 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 ) ) )
79 78 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 ) )
80 14 28 79 syl2an 
 |-  ( ( z e. A /\ w e. A ) -> ( ( x e. z /\ x e. w ) -> z = w ) )
81 12 80 biimtrrid 
 |-  ( ( z e. A /\ w e. A ) -> ( -. ( x e. z -> -. x e. w ) -> z = w ) )
82 81 necon1ad 
 |-  ( ( z e. A /\ w e. A ) -> ( z =/= w -> ( x e. z -> -. x e. w ) ) )
83 82 alrimdv 
 |-  ( ( z e. A /\ w e. A ) -> ( z =/= w -> A. x ( x e. z -> -. x e. w ) ) )
84 disj1 
 |-  ( ( z i^i w ) = (/) <-> A. x ( x e. z -> -. x e. w ) )
85 83 84 imbitrrdi 
 |-  ( ( z e. A /\ w e. A ) -> ( z =/= w -> ( z i^i w ) = (/) ) )
86 85 rgen2 
 |-  A. z e. A A. w e. A ( z =/= w -> ( z i^i w ) = (/) )
87 vex 
 |-  h e. _V
88 vuniex 
 |-  U. h e. _V
89 87 88 xpex 
 |-  ( h X. U. h ) e. _V
90 89 pwex 
 |-  ~P ( h X. U. h ) e. _V
91 snssi 
 |-  ( t e. h -> { t } C_ h )
92 elssuni 
 |-  ( t e. h -> t C_ U. h )
93 xpss12 
 |-  ( ( { t } C_ h /\ t C_ U. h ) -> ( { t } X. t ) C_ ( h X. U. h ) )
94 91 92 93 syl2anc 
 |-  ( t e. h -> ( { t } X. t ) C_ ( h X. U. h ) )
95 vsnex 
 |-  { t } e. _V
96 95 67 xpex 
 |-  ( { t } X. t ) e. _V
97 96 elpw 
 |-  ( ( { t } X. t ) e. ~P ( h X. U. h ) <-> ( { t } X. t ) C_ ( h X. U. h ) )
98 94 97 sylibr 
 |-  ( t e. h -> ( { t } X. t ) e. ~P ( h X. U. h ) )
99 eleq1 
 |-  ( u = ( { t } X. t ) -> ( u e. ~P ( h X. U. h ) <-> ( { t } X. t ) e. ~P ( h X. U. h ) ) )
100 98 99 syl5ibrcom 
 |-  ( t e. h -> ( u = ( { t } X. t ) -> u e. ~P ( h X. U. h ) ) )
101 100 rexlimiv 
 |-  ( E. t e. h u = ( { t } X. t ) -> u e. ~P ( h X. U. h ) )
102 101 adantl 
 |-  ( ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) -> u e. ~P ( h X. U. h ) )
103 102 abssi 
 |-  { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } C_ ~P ( h X. U. h )
104 90 103 ssexi 
 |-  { u | ( u =/= (/) /\ E. t e. h u = ( { t } X. t ) ) } e. _V
105 1 104 eqeltri 
 |-  A e. _V
106 raleq 
 |-  ( x = A -> ( A. z e. x z =/= (/) <-> A. z e. A z =/= (/) ) )
107 raleq 
 |-  ( x = A -> ( A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) <-> A. w e. A ( z =/= w -> ( z i^i w ) = (/) ) ) )
108 107 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 ) = (/) ) ) )
109 106 108 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 ) = (/) ) ) ) )
110 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 ) ) )
111 110 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 ) ) )
112 109 111 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 ) ) ) )
113 105 112 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 ) ) )
114 2 113 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 ) ) )
115 11 86 114 mp2ani 
 |-  ( ph -> E. y A. z e. A E! v v e. ( z i^i y ) )