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

Theorem onfrALTlem5VD 29071
Description: Virtual deduction proof of onfrALTlem5 28702. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem5 28702 is onfrALTlem5VD 29071 without virtual deductions and was automatically derived from onfrALTlem5VD 29071.
1::  |-  a  e.  _V
2:1:  |-  ( a  i^i  x )  e.  _V
3:2:  |-  ( [. ( a  i^i  x )  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =  (/) )
4:3:  |-  ( -.  [. ( a  i^i  x )  /  b ]. b  =  (/)  <->  -.  ( a  i^i  x )  =  (/) )
5::  |-  ( ( a  i^i  x )  =/=  (/)  <->  -.  ( a  i^i  x  )  =  (/) )
6:4,5:  |-  ( -.  [. ( a  i^i  x )  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =/=  (/) )
7:2:  |-  ( -.  [. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  /  b ]. -.  b  =  (/) )
8::  |-  ( b  =/=  (/)  <->  -.  b  =  (/) )
9:8:  |-  A. b ( b  =/=  (/)  <->  -.  b  =  (/) )
10:2,9:  |-  ( [. ( a  i^i  x )  /  b ]. b  =/=  (/)  <->  [. ( a  i^i  x )  /  b ]. -.  b  =  (/) )
11:7,10:  |-  ( -.  [. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  /  b ]. b  =/=  (/) )
12:6,11:  |-  ( [. ( a  i^i  x )  /  b ]. b  =/=  (/)  <->  (  a  i^i  x )  =/=  (/) )
13:2:  |-  ( [. ( a  i^i  x )  /  b ]. b  C_  ( a  i^i  x  )  <->  ( a  i^i  x )  C_  ( a  i^i  x ) )
14:12,13:  |-  ( ( [. ( 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 )  =/=  (/) ) )
15:2:  |-  ( [. ( 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  =/=  (/) ) )
16:15,14:  |-  ( [. ( 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 )  =/=  (/) ) )
17:2:  |-  [_ ( a  i^i  x )  /  b ]_ ( b  i^i  y )  =  (  [_ ( a  i^i  x )  /  b ]_ b  i^i  [_ ( a  i^i  x )  /  b ]_ y )
18:2:  |-  [_ ( a  i^i  x )  /  b ]_ b  =  ( a  i^i  x )
19:2:  |-  [_ ( a  i^i  x )  /  b ]_ y  =  y
20:18,19:  |-  ( [_ ( a  i^i  x )  /  b ]_ b  i^i  [_ ( a  i^i  x )  /  b ]_ y )  =  ( ( a  i^i  x )  i^i  y )
21:17,20:  |-  [_ ( a  i^i  x )  /  b ]_ ( b  i^i  y )  =  ( (  a  i^i  x )  i^i  y )
22:2:  |-  ( [. ( a  i^i  x )  /  b ]. ( b  i^i  y )  =  (/)  <->  [_ ( a  i^i  x )  /  b ]_ ( b  i^i  y )  =  [_ ( a  i^i  x )  /  b ]_  (/) )
23:2:  |-  [_ ( a  i^i  x )  /  b ]_ (/)  =  (/)
24:21,23:  |-  ( [_ ( a  i^i  x )  /  b ]_ ( b  i^i  y )  =  [_ ( a  i^i  x )  /  b ]_ (/)  <->  ( ( a  i^i  x )  i^i  y )  =  (/) )
25:22,24:  |-  ( [. ( a  i^i  x )  /  b ]. ( b  i^i  y )  =  (/)  <->  ( ( a  i^i  x )  i^i  y )  =  (/) )
26:2:  |-  ( [. ( a  i^i  x )  /  b ]. y  e.  b  <->  y  e.  ( a  i^i  x ) )
27:25,26:  |-  ( ( [. ( 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 )  =  (/) ) )
28:2:  |-  ( [. ( 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 )  =  (/) ) )
29:27,28:  |-  ( [. ( 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 )  =  (/) ) )
30:29:  |-  A. y ( [. ( 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 )  =  (/) ) )
31:30:  |-  ( 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 )  =  (/) ) )
32::  |-  ( 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 )  =  (/)  ) )
33:31,32:  |-  ( E. y [. ( a  i^i  x )  /  b ]. ( y  e.  b  /\  ( b  i^i  y )  =  (/) )  <->  E. y  e.  ( a  i^i  x ) ( ( a  i^i  x )  i^i  y )  =  (/) )
34:2:  |-  ( 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 )  =  (/) ) )
35:33,34:  |-  ( [. ( 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  )  =  (/) )
36::  |-  ( E. y  e.  b ( b  i^i  y )  =  (/)  <->  E. y  ( y  e.  b  /\  ( b  i^i  y )  =  (/) ) )
37:36:  |-  A. b ( E. y  e.  b ( b  i^i  y )  =  (/)  <->  E. y ( y  e.  b  /\  ( b  i^i  y )  =  (/) ) )
38:2,37:  |-  ( [. ( 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 )  =  (/) ) )
39:35,38:  |-  ( [. ( 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 )  =  (/) )
40:16,39:  |-  ( ( [. ( 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 )  =  (/) ) )
41: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 )  =  (/) ) )
qed:40,41:  |-  ( [. ( 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 )  =  (/) ) )
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
onfrALTlem5VD  |-  ( [. ( 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 onfrALTlem5VD
StepHypRef Expression
1 vex 2961 . . . 4  |-  a  e. 
_V
21inex1 4347 . . 3  |-  ( a  i^i  x )  e. 
_V
3 sbcimg 3204 . . 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, 3e0_ 28958 . 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 3206 . . . . 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, 5e0_ 28958 . . . 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 3371 . . . . . . 7  |-  ( b  =  ( a  i^i  x )  ->  (
b  C_  ( a  i^i  x )  <->  ( a  i^i  x )  C_  (
a  i^i  x )
) )
87sbcieg 3195 . . . . . 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, 8e0_ 28958 . . . . 5  |-  ( [. ( a  i^i  x
)  /  b ]. b  C_  ( a  i^i  x )  <->  ( a  i^i  x )  C_  (
a  i^i  x )
)
10 sbcng 3203 . . . . . . . . 9  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ].  -.  b  =  (/)  <->  -.  [. (
a  i^i  x )  /  b ]. b  =  (/) ) )
1110bicomd 194 . . . . . . . 8  |-  ( ( a  i^i  x )  e.  _V  ->  ( -.  [. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  / 
b ].  -.  b  =  (/) ) )
122, 11e0_ 28958 . . . . . . 7  |-  ( -. 
[. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  / 
b ].  -.  b  =  (/) )
13 df-ne 2603 . . . . . . . . 9  |-  ( b  =/=  (/)  <->  -.  b  =  (/) )
1413ax-gen 1556 . . . . . . . 8  |-  A. b
( b  =/=  (/)  <->  -.  b  =  (/) )
15 sbcbi 28698 . . . . . . . 8  |-  ( ( a  i^i  x )  e.  _V  ->  ( A. b ( b  =/=  (/) 
<->  -.  b  =  (/) )  ->  ( [. (
a  i^i  x )  /  b ]. b  =/=  (/)  <->  [. ( a  i^i  x )  /  b ].  -.  b  =  (/) ) ) )
162, 14, 15e00 28954 . . . . . . 7  |-  ( [. ( a  i^i  x
)  /  b ]. b  =/=  (/)  <->  [. ( a  i^i  x )  /  b ].  -.  b  =  (/) )
1712, 16bitr4i 245 . . . . . 6  |-  ( -. 
[. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  / 
b ]. b  =/=  (/) )
18 eqsbc3 3202 . . . . . . . . 9  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =  (/) ) )
192, 18e0_ 28958 . . . . . . . 8  |-  ( [. ( a  i^i  x
)  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =  (/) )
2019notbii 289 . . . . . . 7  |-  ( -. 
[. ( a  i^i  x )  /  b ]. b  =  (/)  <->  -.  (
a  i^i  x )  =  (/) )
21 df-ne 2603 . . . . . . 7  |-  ( ( a  i^i  x )  =/=  (/)  <->  -.  ( a  i^i  x )  =  (/) )
2220, 21bitr4i 245 . . . . . 6  |-  ( -. 
[. ( a  i^i  x )  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =/=  (/) )
2317, 22bitr3i 244 . . . . 5  |-  ( [. ( a  i^i  x
)  /  b ]. b  =/=  (/)  <->  ( a  i^i  x )  =/=  (/) )
249, 23anbi12i 680 . . . 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 )  =/=  (/) ) )
256, 24bitri 242 . . 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 )  =/=  (/) ) )
26 df-rex 2713 . . . . . 6  |-  ( E. y  e.  b  ( b  i^i  y )  =  (/)  <->  E. y ( y  e.  b  /\  (
b  i^i  y )  =  (/) ) )
2726ax-gen 1556 . . . . 5  |-  A. b
( E. y  e.  b  ( b  i^i  y )  =  (/)  <->  E. y ( y  e.  b  /\  ( b  i^i  y )  =  (/) ) )
28 sbcbi 28698 . . . . 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
)  =  (/) ) ) ) )
292, 27, 28e00 28954 . . . 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
)  =  (/) ) )
30 sbcexg 3213 . . . . . . 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
)  =  (/) ) ) )
3130bicomd 194 . . . . . 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 )  =  (/) ) ) )
322, 31e0_ 28958 . . . . 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 )  =  (/) ) )
33 sbcang 3206 . . . . . . . . . 10  |-  ( ( 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 )  =  (/) ) ) )
342, 33e0_ 28958 . . . . . . . . 9  |-  ( [. ( 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 )  =  (/) ) )
35 sbcel2gv 3223 . . . . . . . . . . 11  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ]. y  e.  b  <->  y  e.  ( a  i^i  x
) ) )
362, 35e0_ 28958 . . . . . . . . . 10  |-  ( [. ( a  i^i  x
)  /  b ]. y  e.  b  <->  y  e.  ( a  i^i  x
) )
37 sbceqg 3269 . . . . . . . . . . . 12  |-  ( ( 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 ]_ (/) ) )
382, 37e0_ 28958 . . . . . . . . . . 11  |-  ( [. ( a  i^i  x
)  /  b ]. ( b  i^i  y
)  =  (/)  <->  [_ ( a  i^i  x )  / 
b ]_ ( b  i^i  y )  =  [_ ( a  i^i  x
)  /  b ]_ (/) )
39 csbing 3550 . . . . . . . . . . . . . 14  |-  ( ( 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 ) )
402, 39e0_ 28958 . . . . . . . . . . . . 13  |-  [_ (
a  i^i  x )  /  b ]_ (
b  i^i  y )  =  ( [_ (
a  i^i  x )  /  b ]_ b  i^i  [_ ( a  i^i  x )  /  b ]_ y )
41 csbvarg 3280 . . . . . . . . . . . . . . 15  |-  ( ( a  i^i  x )  e.  _V  ->  [_ (
a  i^i  x )  /  b ]_ b  =  ( a  i^i  x ) )
422, 41e0_ 28958 . . . . . . . . . . . . . 14  |-  [_ (
a  i^i  x )  /  b ]_ b  =  ( a  i^i  x )
43 csbconstg 3267 . . . . . . . . . . . . . . 15  |-  ( ( a  i^i  x )  e.  _V  ->  [_ (
a  i^i  x )  /  b ]_ y  =  y )
442, 43e0_ 28958 . . . . . . . . . . . . . 14  |-  [_ (
a  i^i  x )  /  b ]_ y  =  y
4542, 44ineq12i 3542 . . . . . . . . . . . . 13  |-  ( [_ ( a  i^i  x
)  /  b ]_ b  i^i  [_ ( a  i^i  x )  /  b ]_ y )  =  ( ( a  i^i  x
)  i^i  y )
4640, 45eqtri 2458 . . . . . . . . . . . 12  |-  [_ (
a  i^i  x )  /  b ]_ (
b  i^i  y )  =  ( ( a  i^i  x )  i^i  y )
47 csbconstg 3267 . . . . . . . . . . . . 13  |-  ( ( a  i^i  x )  e.  _V  ->  [_ (
a  i^i  x )  /  b ]_ (/)  =  (/) )
482, 47e0_ 28958 . . . . . . . . . . . 12  |-  [_ (
a  i^i  x )  /  b ]_ (/)  =  (/)
4946, 48eqeq12i 2451 . . . . . . . . . . 11  |-  ( [_ ( a  i^i  x
)  /  b ]_ ( b  i^i  y
)  =  [_ (
a  i^i  x )  /  b ]_ (/)  <->  ( (
a  i^i  x )  i^i  y )  =  (/) )
5038, 49bitri 242 . . . . . . . . . 10  |-  ( [. ( a  i^i  x
)  /  b ]. ( b  i^i  y
)  =  (/)  <->  ( (
a  i^i  x )  i^i  y )  =  (/) )
5136, 50anbi12i 680 . . . . . . . . 9  |-  ( (
[. ( 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 )  =  (/) ) )
5234, 51bitri 242 . . . . . . . 8  |-  ( [. ( 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 )  =  (/) ) )
5352ax-gen 1556 . . . . . . 7  |-  A. y
( [. ( 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 )  =  (/) ) )
54 exbi 1592 . . . . . . 7  |-  ( A. y ( [. (
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 )  =  (/) ) )  ->  ( 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 )  =  (/) ) ) )
5553, 54e0_ 28958 . . . . . 6  |-  ( 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 )  =  (/) ) )
56 df-rex 2713 . . . . . 6  |-  ( 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 )  =  (/) ) )
5755, 56bitr4i 245 . . . . 5  |-  ( E. y [. ( a  i^i  x )  / 
b ]. ( y  e.  b  /\  ( b  i^i  y )  =  (/) )  <->  E. y  e.  ( a  i^i  x ) ( ( a  i^i  x )  i^i  y
)  =  (/) )
5832, 57bitr3i 244 . . . 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
)  =  (/) )
5929, 58bitri 242 . . 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 )  =  (/) )
6025, 59imbi12i 318 . 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 )  =  (/) ) )
614, 60bitri 242 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 178    /\ wa 360   A.wal 1550   E.wex 1551    = wceq 1653    e. wcel 1726    =/= wne 2601   E.wrex 2708   _Vcvv 2958   [.wsbc 3163   [_csb 3253    i^i cin 3321    C_ wss 3322   (/)c0 3630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator