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

Theorem onfrALTlem5VD 37345
Description: Virtual deduction proof of onfrALTlem5 36978. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem5 36978 is onfrALTlem5VD 37345 without virtual deductions and was automatically derived from onfrALTlem5VD 37345.
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 3034 . . . 4  |-  a  e. 
_V
21inex1 4537 . . 3  |-  ( a  i^i  x )  e. 
_V
3 sbcimg 3297 . . 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, 3e0a 37222 . 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 sbcangOLD 36960 . . . . 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, 5e0a 37222 . . . 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 3439 . . . . . . 7  |-  ( b  =  ( a  i^i  x )  ->  (
b  C_  ( a  i^i  x )  <->  ( a  i^i  x )  C_  (
a  i^i  x )
) )
87sbcieg 3288 . . . . . 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, 8e0a 37222 . . . . 5  |-  ( [. ( a  i^i  x
)  /  b ]. b  C_  ( a  i^i  x )  <->  ( a  i^i  x )  C_  (
a  i^i  x )
)
10 sbcng 3296 . . . . . . . . 9  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ].  -.  b  =  (/)  <->  -.  [. (
a  i^i  x )  /  b ]. b  =  (/) ) )
1110bicomd 206 . . . . . . . 8  |-  ( ( a  i^i  x )  e.  _V  ->  ( -.  [. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  / 
b ].  -.  b  =  (/) ) )
122, 11e0a 37222 . . . . . . 7  |-  ( -. 
[. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  / 
b ].  -.  b  =  (/) )
13 df-ne 2643 . . . . . . . . 9  |-  ( b  =/=  (/)  <->  -.  b  =  (/) )
1413ax-gen 1677 . . . . . . . 8  |-  A. b
( b  =/=  (/)  <->  -.  b  =  (/) )
15 sbcbi 36970 . . . . . . . 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 37218 . . . . . . 7  |-  ( [. ( a  i^i  x
)  /  b ]. b  =/=  (/)  <->  [. ( a  i^i  x )  /  b ].  -.  b  =  (/) )
1712, 16bitr4i 260 . . . . . 6  |-  ( -. 
[. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  / 
b ]. b  =/=  (/) )
18 eqsbc3 3295 . . . . . . . . 9  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =  (/) ) )
192, 18e0a 37222 . . . . . . . 8  |-  ( [. ( a  i^i  x
)  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =  (/) )
2019notbii 303 . . . . . . 7  |-  ( -. 
[. ( a  i^i  x )  /  b ]. b  =  (/)  <->  -.  (
a  i^i  x )  =  (/) )
21 df-ne 2643 . . . . . . 7  |-  ( ( a  i^i  x )  =/=  (/)  <->  -.  ( a  i^i  x )  =  (/) )
2220, 21bitr4i 260 . . . . . 6  |-  ( -. 
[. ( a  i^i  x )  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =/=  (/) )
2317, 22bitr3i 259 . . . . 5  |-  ( [. ( a  i^i  x
)  /  b ]. b  =/=  (/)  <->  ( a  i^i  x )  =/=  (/) )
249, 23anbi12i 711 . . . 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 257 . . 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 2762 . . . . . 6  |-  ( E. y  e.  b  ( b  i^i  y )  =  (/)  <->  E. y ( y  e.  b  /\  (
b  i^i  y )  =  (/) ) )
2726ax-gen 1677 . . . . 5  |-  A. b
( E. y  e.  b  ( b  i^i  y )  =  (/)  <->  E. y ( y  e.  b  /\  ( b  i^i  y )  =  (/) ) )
28 sbcbi 36970 . . . . 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 37218 . . . 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 sbcexgOLD 36974 . . . . . . 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 206 . . . . . 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, 31e0a 37222 . . . . 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 sbcangOLD 36960 . . . . . . . . . 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, 33e0a 37222 . . . . . . . . 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 3315 . . . . . . . . . . 11  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ]. y  e.  b  <->  y  e.  ( a  i^i  x
) ) )
362, 35e0a 37222 . . . . . . . . . 10  |-  ( [. ( a  i^i  x
)  /  b ]. y  e.  b  <->  y  e.  ( a  i^i  x
) )
37 sbceqg 3777 . . . . . . . . . . . 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, 37e0a 37222 . . . . . . . . . . 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 csbingOLD 37278 . . . . . . . . . . . . . 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, 39e0a 37222 . . . . . . . . . . . . 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 3796 . . . . . . . . . . . . . . 15  |-  ( ( a  i^i  x )  e.  _V  ->  [_ (
a  i^i  x )  /  b ]_ b  =  ( a  i^i  x ) )
422, 41e0a 37222 . . . . . . . . . . . . . 14  |-  [_ (
a  i^i  x )  /  b ]_ b  =  ( a  i^i  x )
43 csbconstg 3362 . . . . . . . . . . . . . . 15  |-  ( ( a  i^i  x )  e.  _V  ->  [_ (
a  i^i  x )  /  b ]_ y  =  y )
442, 43e0a 37222 . . . . . . . . . . . . . 14  |-  [_ (
a  i^i  x )  /  b ]_ y  =  y
4542, 44ineq12i 3623 . . . . . . . . . . . . 13  |-  ( [_ ( a  i^i  x
)  /  b ]_ b  i^i  [_ ( a  i^i  x )  /  b ]_ y )  =  ( ( a  i^i  x
)  i^i  y )
4640, 45eqtri 2493 . . . . . . . . . . . 12  |-  [_ (
a  i^i  x )  /  b ]_ (
b  i^i  y )  =  ( ( a  i^i  x )  i^i  y )
47 csbconstg 3362 . . . . . . . . . . . . 13  |-  ( ( a  i^i  x )  e.  _V  ->  [_ (
a  i^i  x )  /  b ]_ (/)  =  (/) )
482, 47e0a 37222 . . . . . . . . . . . 12  |-  [_ (
a  i^i  x )  /  b ]_ (/)  =  (/)
4946, 48eqeq12i 2485 . . . . . . . . . . 11  |-  ( [_ ( a  i^i  x
)  /  b ]_ ( b  i^i  y
)  =  [_ (
a  i^i  x )  /  b ]_ (/)  <->  ( (
a  i^i  x )  i^i  y )  =  (/) )
5038, 49bitri 257 . . . . . . . . . 10  |-  ( [. ( a  i^i  x
)  /  b ]. ( b  i^i  y
)  =  (/)  <->  ( (
a  i^i  x )  i^i  y )  =  (/) )
5136, 50anbi12i 711 . . . . . . . . 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 257 . . . . . . . 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 1677 . . . . . . 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 1724 . . . . . . 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, 54e0a 37222 . . . . . 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 2762 . . . . . 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 260 . . . . 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 259 . . . 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 257 . . 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 333 . 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 257 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 setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    /\ wa 376   A.wal 1450    = wceq 1452   E.wex 1671    e. wcel 1904    =/= wne 2641   E.wrex 2757   _Vcvv 3031   [.wsbc 3255   [_csb 3349    i^i cin 3389    C_ wss 3390   (/)c0 3722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-in 3397  df-ss 3404
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator