Metamath Proof Explorer

Theorem onfrALTlem5

Description: Lemma for onfrALT . (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 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 ) = (/) ) )

Proof

Step Hyp Ref Expression
1 vex 
 |-  a e. _V
2 1 inex1 
 |-  ( a i^i x ) e. _V
3 sbcimg 
 |-  ( ( 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 ) = (/) ) ) )
4 2 3 ax-mp 
 |-  ( [. ( 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 sbcan 
 |-  ( [. ( 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 =/= (/) ) )
6 sseq1 
 |-  ( b = ( a i^i x ) -> ( b C_ ( a i^i x ) <-> ( a i^i x ) C_ ( a i^i x ) ) )
7 2 6 sbcie 
 |-  ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) <-> ( a i^i x ) C_ ( a i^i x ) )
8 df-ne 
 |-  ( b =/= (/) <-> -. b = (/) )
9 8 sbcbii 
 |-  ( [. ( a i^i x ) / b ]. b =/= (/) <-> [. ( a i^i x ) / b ]. -. b = (/) )
10 sbcng 
 |-  ( ( a i^i x ) e. _V -> ( [. ( a i^i x ) / b ]. -. b = (/) <-> -. [. ( a i^i x ) / b ]. b = (/) ) )
11 10 bicomd 
 |-  ( ( a i^i x ) e. _V -> ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. -. b = (/) ) )
12 2 11 ax-mp 
 |-  ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. -. b = (/) )
13 eqsbc1 
 |-  ( ( a i^i x ) e. _V -> ( [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) = (/) ) )
14 2 13 ax-mp 
 |-  ( [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) = (/) )
15 14 necon3bbii 
 |-  ( -. [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) =/= (/) )
16 9 12 15 3bitr2i 
 |-  ( [. ( a i^i x ) / b ]. b =/= (/) <-> ( a i^i x ) =/= (/) )
17 7 16 anbi12i 
 |-  ( ( [. ( 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 ) =/= (/) ) )
18 5 17 bitri 
 |-  ( [. ( 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 ) =/= (/) ) )
19 df-rex 
 |-  ( E. y e. b ( b i^i y ) = (/) <-> E. y ( y e. b /\ ( b i^i y ) = (/) ) )
20 19 sbcbii 
 |-  ( [. ( 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 ) = (/) ) )
21 sbcan 
 |-  ( [. ( 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 ) = (/) ) )
22 sbcel2gv 
 |-  ( ( a i^i x ) e. _V -> ( [. ( a i^i x ) / b ]. y e. b <-> y e. ( a i^i x ) ) )
23 2 22 ax-mp 
 |-  ( [. ( a i^i x ) / b ]. y e. b <-> y e. ( a i^i x ) )
24 sbceqg 
 |-  ( ( 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 ]_ (/) ) )
25 2 24 ax-mp 
 |-  ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) )
26 csbin 
 |-  [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y )
27 csbvarg 
 |-  ( ( a i^i x ) e. _V -> [_ ( a i^i x ) / b ]_ b = ( a i^i x ) )
28 2 27 ax-mp 
 |-  [_ ( a i^i x ) / b ]_ b = ( a i^i x )
29 csbconstg 
 |-  ( ( a i^i x ) e. _V -> [_ ( a i^i x ) / b ]_ y = y )
30 2 29 ax-mp 
 |-  [_ ( a i^i x ) / b ]_ y = y
31 28 30 ineq12i 
 |-  ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y ) = ( ( a i^i x ) i^i y )
32 26 31 eqtri 
 |-  [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( ( a i^i x ) i^i y )
33 csb0 
 |-  [_ ( a i^i x ) / b ]_ (/) = (/)
34 32 33 eqeq12i 
 |-  ( [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) <-> ( ( a i^i x ) i^i y ) = (/) )
35 25 34 bitri 
 |-  ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> ( ( a i^i x ) i^i y ) = (/) )
36 23 35 anbi12i 
 |-  ( ( [. ( 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 ) = (/) ) )
37 21 36 bitri 
 |-  ( [. ( 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 ) = (/) ) )
38 37 exbii 
 |-  ( 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 ) = (/) ) )
39 sbcex2 
 |-  ( [. ( 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 ) = (/) ) )
40 df-rex 
 |-  ( 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 ) = (/) ) )
41 38 39 40 3bitr4i 
 |-  ( [. ( 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 ) = (/) )
42 20 41 bitri 
 |-  ( [. ( 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 ) = (/) )
43 18 42 imbi12i 
 |-  ( ( [. ( 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 ) = (/) ) )
44 4 43 bitri 
 |-  ( [. ( 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 ) = (/) ) )