Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  onfrALTlem5 Unicode version

Theorem onfrALTlem5 28307
Description: Lemma for onfrALT 28314. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
onfrALTlem5  |-  ( [. ( a  i^i  x
)  /  b ]. ( ( b  C_  ( a  i^i  x
)  /\  b  =/=  (/) )  ->  E. y  e.  b  ( b  i^i  y )  =  (/) ) 
<->  ( ( ( a  i^i  x )  C_  ( a  i^i  x
)  /\  ( a  i^i  x )  =/=  (/) )  ->  E. y  e.  (
a  i^i  x )
( ( a  i^i  x )  i^i  y
)  =  (/) ) )
Distinct variable groups:    a, b,
y    x, b, y

Proof of Theorem onfrALTlem5
StepHypRef Expression
1 vex 2791 . . . 4  |-  a  e. 
_V
21inex1 4155 . . 3  |-  ( a  i^i  x )  e. 
_V
3 sbcimg 3032 . . 3  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ]. ( ( b  C_  ( a  i^i  x
)  /\  b  =/=  (/) )  ->  E. y  e.  b  ( b  i^i  y )  =  (/) ) 
<->  ( [. ( a  i^i  x )  / 
b ]. ( b  C_  ( a  i^i  x
)  /\  b  =/=  (/) )  ->  [. ( a  i^i  x )  / 
b ]. E. y  e.  b  ( b  i^i  y )  =  (/) ) ) )
42, 3ax-mp 8 . 2  |-  ( [. ( a  i^i  x
)  /  b ]. ( ( b  C_  ( a  i^i  x
)  /\  b  =/=  (/) )  ->  E. y  e.  b  ( b  i^i  y )  =  (/) ) 
<->  ( [. ( a  i^i  x )  / 
b ]. ( b  C_  ( a  i^i  x
)  /\  b  =/=  (/) )  ->  [. ( a  i^i  x )  / 
b ]. E. y  e.  b  ( b  i^i  y )  =  (/) ) )
5 sbcang 3034 . . . . 5  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ]. ( b  C_  (
a  i^i  x )  /\  b  =/=  (/) )  <->  ( [. ( a  i^i  x
)  /  b ]. b  C_  ( a  i^i  x )  /\  [. (
a  i^i  x )  /  b ]. b  =/=  (/) ) ) )
62, 5ax-mp 8 . . . 4  |-  ( [. ( a  i^i  x
)  /  b ]. ( b  C_  (
a  i^i  x )  /\  b  =/=  (/) )  <->  ( [. ( a  i^i  x
)  /  b ]. b  C_  ( a  i^i  x )  /\  [. (
a  i^i  x )  /  b ]. b  =/=  (/) ) )
7 sseq1 3199 . . . . . . 7  |-  ( b  =  ( a  i^i  x )  ->  (
b  C_  ( a  i^i  x )  <->  ( a  i^i  x )  C_  (
a  i^i  x )
) )
87sbcieg 3023 . . . . . 6  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ]. b  C_  ( a  i^i  x )  <->  ( a  i^i  x )  C_  (
a  i^i  x )
) )
92, 8ax-mp 8 . . . . 5  |-  ( [. ( a  i^i  x
)  /  b ]. b  C_  ( a  i^i  x )  <->  ( a  i^i  x )  C_  (
a  i^i  x )
)
10 df-ne 2448 . . . . . . . 8  |-  ( b  =/=  (/)  <->  -.  b  =  (/) )
1110ax-gen 1533 . . . . . . 7  |-  A. b
( b  =/=  (/)  <->  -.  b  =  (/) )
12 sbcbi 28303 . . . . . . 7  |-  ( ( a  i^i  x )  e.  _V  ->  ( A. b ( b  =/=  (/) 
<->  -.  b  =  (/) )  ->  ( [. (
a  i^i  x )  /  b ]. b  =/=  (/)  <->  [. ( a  i^i  x )  /  b ].  -.  b  =  (/) ) ) )
132, 11, 12mp2 17 . . . . . 6  |-  ( [. ( a  i^i  x
)  /  b ]. b  =/=  (/)  <->  [. ( a  i^i  x )  /  b ].  -.  b  =  (/) )
14 sbcng 3031 . . . . . . . 8  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ].  -.  b  =  (/)  <->  -.  [. (
a  i^i  x )  /  b ]. b  =  (/) ) )
1514bicomd 192 . . . . . . 7  |-  ( ( a  i^i  x )  e.  _V  ->  ( -.  [. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  / 
b ].  -.  b  =  (/) ) )
162, 15ax-mp 8 . . . . . 6  |-  ( -. 
[. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  / 
b ].  -.  b  =  (/) )
17 eqsbc3 3030 . . . . . . . 8  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =  (/) ) )
182, 17ax-mp 8 . . . . . . 7  |-  ( [. ( a  i^i  x
)  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =  (/) )
1918necon3bbii 2477 . . . . . 6  |-  ( -. 
[. ( a  i^i  x )  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =/=  (/) )
2013, 16, 193bitr2i 264 . . . . 5  |-  ( [. ( a  i^i  x
)  /  b ]. b  =/=  (/)  <->  ( a  i^i  x )  =/=  (/) )
219, 20anbi12i 678 . . . 4  |-  ( (
[. ( a  i^i  x )  /  b ]. b  C_  ( a  i^i  x )  /\  [. ( a  i^i  x
)  /  b ]. b  =/=  (/) )  <->  ( (
a  i^i  x )  C_  ( a  i^i  x
)  /\  ( a  i^i  x )  =/=  (/) ) )
226, 21bitri 240 . . 3  |-  ( [. ( a  i^i  x
)  /  b ]. ( b  C_  (
a  i^i  x )  /\  b  =/=  (/) )  <->  ( (
a  i^i  x )  C_  ( a  i^i  x
)  /\  ( a  i^i  x )  =/=  (/) ) )
23 df-rex 2549 . . . . . 6  |-  ( E. y  e.  b  ( b  i^i  y )  =  (/)  <->  E. y ( y  e.  b  /\  (
b  i^i  y )  =  (/) ) )
2423ax-gen 1533 . . . . 5  |-  A. b
( E. y  e.  b  ( b  i^i  y )  =  (/)  <->  E. y ( y  e.  b  /\  ( b  i^i  y )  =  (/) ) )
25 sbcbi 28303 . . . . 5  |-  ( ( a  i^i  x )  e.  _V  ->  ( A. b ( E. y  e.  b  ( b  i^i  y )  =  (/)  <->  E. y ( y  e.  b  /\  ( b  i^i  y )  =  (/) ) )  ->  ( [. ( a  i^i  x
)  /  b ]. E. y  e.  b 
( b  i^i  y
)  =  (/)  <->  [. ( a  i^i  x )  / 
b ]. E. y ( y  e.  b  /\  ( b  i^i  y
)  =  (/) ) ) ) )
262, 24, 25mp2 17 . . . 4  |-  ( [. ( a  i^i  x
)  /  b ]. E. y  e.  b 
( b  i^i  y
)  =  (/)  <->  [. ( a  i^i  x )  / 
b ]. E. y ( y  e.  b  /\  ( b  i^i  y
)  =  (/) ) )
27 df-rex 2549 . . . . 5  |-  ( E. y  e.  ( a  i^i  x ) ( ( a  i^i  x
)  i^i  y )  =  (/)  <->  E. y ( y  e.  ( a  i^i  x )  /\  (
( a  i^i  x
)  i^i  y )  =  (/) ) )
28 sbcang 3034 . . . . . . . 8  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ]. ( y  e.  b  /\  ( b  i^i  y )  =  (/) ) 
<->  ( [. ( a  i^i  x )  / 
b ]. y  e.  b  /\  [. ( a  i^i  x )  / 
b ]. ( b  i^i  y )  =  (/) ) ) )
292, 28ax-mp 8 . . . . . . 7  |-  ( [. ( a  i^i  x
)  /  b ]. ( y  e.  b  /\  ( b  i^i  y )  =  (/) ) 
<->  ( [. ( a  i^i  x )  / 
b ]. y  e.  b  /\  [. ( a  i^i  x )  / 
b ]. ( b  i^i  y )  =  (/) ) )
30 sbcel2gv 3051 . . . . . . . . 9  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ]. y  e.  b  <->  y  e.  ( a  i^i  x
) ) )
312, 30ax-mp 8 . . . . . . . 8  |-  ( [. ( a  i^i  x
)  /  b ]. y  e.  b  <->  y  e.  ( a  i^i  x
) )
32 sbceqg 3097 . . . . . . . . . 10  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ]. ( b  i^i  y
)  =  (/)  <->  [_ ( a  i^i  x )  / 
b ]_ ( b  i^i  y )  =  [_ ( a  i^i  x
)  /  b ]_ (/) ) )
332, 32ax-mp 8 . . . . . . . . 9  |-  ( [. ( a  i^i  x
)  /  b ]. ( b  i^i  y
)  =  (/)  <->  [_ ( a  i^i  x )  / 
b ]_ ( b  i^i  y )  =  [_ ( a  i^i  x
)  /  b ]_ (/) )
34 csbing 3376 . . . . . . . . . . . 12  |-  ( ( a  i^i  x )  e.  _V  ->  [_ (
a  i^i  x )  /  b ]_ (
b  i^i  y )  =  ( [_ (
a  i^i  x )  /  b ]_ b  i^i  [_ ( a  i^i  x )  /  b ]_ y ) )
352, 34ax-mp 8 . . . . . . . . . . 11  |-  [_ (
a  i^i  x )  /  b ]_ (
b  i^i  y )  =  ( [_ (
a  i^i  x )  /  b ]_ b  i^i  [_ ( a  i^i  x )  /  b ]_ y )
36 csbvarg 3108 . . . . . . . . . . . . 13  |-  ( ( a  i^i  x )  e.  _V  ->  [_ (
a  i^i  x )  /  b ]_ b  =  ( a  i^i  x ) )
372, 36ax-mp 8 . . . . . . . . . . . 12  |-  [_ (
a  i^i  x )  /  b ]_ b  =  ( a  i^i  x )
38 csbconstg 3095 . . . . . . . . . . . . 13  |-  ( ( a  i^i  x )  e.  _V  ->  [_ (
a  i^i  x )  /  b ]_ y  =  y )
392, 38ax-mp 8 . . . . . . . . . . . 12  |-  [_ (
a  i^i  x )  /  b ]_ y  =  y
4037, 39ineq12i 3368 . . . . . . . . . . 11  |-  ( [_ ( a  i^i  x
)  /  b ]_ b  i^i  [_ ( a  i^i  x )  /  b ]_ y )  =  ( ( a  i^i  x
)  i^i  y )
4135, 40eqtri 2303 . . . . . . . . . 10  |-  [_ (
a  i^i  x )  /  b ]_ (
b  i^i  y )  =  ( ( a  i^i  x )  i^i  y )
42 csbconstg 3095 . . . . . . . . . . 11  |-  ( ( a  i^i  x )  e.  _V  ->  [_ (
a  i^i  x )  /  b ]_ (/)  =  (/) )
432, 42ax-mp 8 . . . . . . . . . 10  |-  [_ (
a  i^i  x )  /  b ]_ (/)  =  (/)
4441, 43eqeq12i 2296 . . . . . . . . 9  |-  ( [_ ( a  i^i  x
)  /  b ]_ ( b  i^i  y
)  =  [_ (
a  i^i  x )  /  b ]_ (/)  <->  ( (
a  i^i  x )  i^i  y )  =  (/) )
4533, 44bitri 240 . . . . . . . 8  |-  ( [. ( a  i^i  x
)  /  b ]. ( b  i^i  y
)  =  (/)  <->  ( (
a  i^i  x )  i^i  y )  =  (/) )
4631, 45anbi12i 678 . . . . . . 7  |-  ( (
[. ( a  i^i  x )  /  b ]. y  e.  b  /\  [. ( a  i^i  x )  /  b ]. ( b  i^i  y
)  =  (/) )  <->  ( y  e.  ( a  i^i  x
)  /\  ( (
a  i^i  x )  i^i  y )  =  (/) ) )
4729, 46bitri 240 . . . . . 6  |-  ( [. ( a  i^i  x
)  /  b ]. ( y  e.  b  /\  ( b  i^i  y )  =  (/) ) 
<->  ( y  e.  ( a  i^i  x )  /\  ( ( a  i^i  x )  i^i  y )  =  (/) ) )
4847exbii 1569 . . . . 5  |-  ( E. y [. ( a  i^i  x )  / 
b ]. ( y  e.  b  /\  ( b  i^i  y )  =  (/) )  <->  E. y ( y  e.  ( a  i^i  x )  /\  (
( a  i^i  x
)  i^i  y )  =  (/) ) )
49 sbcexg 3041 . . . . . . 7  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ]. E. y ( y  e.  b  /\  ( b  i^i  y )  =  (/) )  <->  E. y [. (
a  i^i  x )  /  b ]. (
y  e.  b  /\  ( b  i^i  y
)  =  (/) ) ) )
5049bicomd 192 . . . . . 6  |-  ( ( a  i^i  x )  e.  _V  ->  ( E. y [. ( a  i^i  x )  / 
b ]. ( y  e.  b  /\  ( b  i^i  y )  =  (/) )  <->  [. ( a  i^i  x )  /  b ]. E. y ( y  e.  b  /\  (
b  i^i  y )  =  (/) ) ) )
512, 50ax-mp 8 . . . . 5  |-  ( E. y [. ( a  i^i  x )  / 
b ]. ( y  e.  b  /\  ( b  i^i  y )  =  (/) )  <->  [. ( a  i^i  x )  /  b ]. E. y ( y  e.  b  /\  (
b  i^i  y )  =  (/) ) )
5227, 48, 513bitr2ri 265 . . . 4  |-  ( [. ( a  i^i  x
)  /  b ]. E. y ( y  e.  b  /\  ( b  i^i  y )  =  (/) )  <->  E. y  e.  ( a  i^i  x ) ( ( a  i^i  x )  i^i  y
)  =  (/) )
5326, 52bitri 240 . . 3  |-  ( [. ( a  i^i  x
)  /  b ]. E. y  e.  b 
( b  i^i  y
)  =  (/)  <->  E. y  e.  ( a  i^i  x
) ( ( a  i^i  x )  i^i  y )  =  (/) )
5422, 53imbi12i 316 . 2  |-  ( (
[. ( a  i^i  x )  /  b ]. ( b  C_  (
a  i^i  x )  /\  b  =/=  (/) )  ->  [. ( a  i^i  x
)  /  b ]. E. y  e.  b 
( b  i^i  y
)  =  (/) )  <->  ( (
( a  i^i  x
)  C_  ( a  i^i  x )  /\  (
a  i^i  x )  =/=  (/) )  ->  E. y  e.  ( a  i^i  x
) ( ( a  i^i  x )  i^i  y )  =  (/) ) )
554, 54bitri 240 1  |-  ( [. ( a  i^i  x
)  /  b ]. ( ( b  C_  ( a  i^i  x
)  /\  b  =/=  (/) )  ->  E. y  e.  b  ( b  i^i  y )  =  (/) ) 
<->  ( ( ( a  i^i  x )  C_  ( a  i^i  x
)  /\  ( a  i^i  x )  =/=  (/) )  ->  E. y  e.  (
a  i^i  x )
( ( a  i^i  x )  i^i  y
)  =  (/) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1527   E.wex 1528    = wceq 1623    e. wcel 1684    =/= wne 2446   E.wrex 2544   _Vcvv 2788   [.wsbc 2991   [_csb 3081    i^i cin 3151    C_ wss 3152   (/)c0 3455
This theorem is referenced by:  onfrALTlem3  28309  onfrALTlem3VD  28663
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator