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

Theorem onfrALTlem5VD 31626
Description: Virtual deduction proof of onfrALTlem5 31255. 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 31255 is onfrALTlem5VD 31626 without virtual deductions and was automatically derived from onfrALTlem5VD 31626.
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 2980 . . . 4  |-  a  e. 
_V
21inex1 4438 . . 3  |-  ( a  i^i  x )  e. 
_V
3 sbcimg 3233 . . 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 31510 . 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 3235 . . . . 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 31510 . . . 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 3382 . . . . . . 7  |-  ( b  =  ( a  i^i  x )  ->  (
b  C_  ( a  i^i  x )  <->  ( a  i^i  x )  C_  (
a  i^i  x )
) )
87sbcieg 3224 . . . . . 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 31510 . . . . 5  |-  ( [. ( a  i^i  x
)  /  b ]. b  C_  ( a  i^i  x )  <->  ( a  i^i  x )  C_  (
a  i^i  x )
)
10 sbcng 3232 . . . . . . . . 9  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ].  -.  b  =  (/)  <->  -.  [. (
a  i^i  x )  /  b ]. b  =  (/) ) )
1110bicomd 201 . . . . . . . 8  |-  ( ( a  i^i  x )  e.  _V  ->  ( -.  [. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  / 
b ].  -.  b  =  (/) ) )
122, 11e0a 31510 . . . . . . 7  |-  ( -. 
[. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  / 
b ].  -.  b  =  (/) )
13 df-ne 2613 . . . . . . . . 9  |-  ( b  =/=  (/)  <->  -.  b  =  (/) )
1413ax-gen 1591 . . . . . . . 8  |-  A. b
( b  =/=  (/)  <->  -.  b  =  (/) )
15 sbcbi 31251 . . . . . . . 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 31506 . . . . . . 7  |-  ( [. ( a  i^i  x
)  /  b ]. b  =/=  (/)  <->  [. ( a  i^i  x )  /  b ].  -.  b  =  (/) )
1712, 16bitr4i 252 . . . . . 6  |-  ( -. 
[. ( a  i^i  x )  /  b ]. b  =  (/)  <->  [. ( a  i^i  x )  / 
b ]. b  =/=  (/) )
18 eqsbc3 3231 . . . . . . . . 9  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =  (/) ) )
192, 18e0a 31510 . . . . . . . 8  |-  ( [. ( a  i^i  x
)  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =  (/) )
2019notbii 296 . . . . . . 7  |-  ( -. 
[. ( a  i^i  x )  /  b ]. b  =  (/)  <->  -.  (
a  i^i  x )  =  (/) )
21 df-ne 2613 . . . . . . 7  |-  ( ( a  i^i  x )  =/=  (/)  <->  -.  ( a  i^i  x )  =  (/) )
2220, 21bitr4i 252 . . . . . 6  |-  ( -. 
[. ( a  i^i  x )  /  b ]. b  =  (/)  <->  ( a  i^i  x )  =/=  (/) )
2317, 22bitr3i 251 . . . . 5  |-  ( [. ( a  i^i  x
)  /  b ]. b  =/=  (/)  <->  ( a  i^i  x )  =/=  (/) )
249, 23anbi12i 697 . . . 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 249 . . 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 2726 . . . . . 6  |-  ( E. y  e.  b  ( b  i^i  y )  =  (/)  <->  E. y ( y  e.  b  /\  (
b  i^i  y )  =  (/) ) )
2726ax-gen 1591 . . . . 5  |-  A. b
( E. y  e.  b  ( b  i^i  y )  =  (/)  <->  E. y ( y  e.  b  /\  ( b  i^i  y )  =  (/) ) )
28 sbcbi 31251 . . . . 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 31506 . . . 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 3246 . . . . . . 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 201 . . . . . 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 31510 . . . . 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 3235 . . . . . . . . . 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 31510 . . . . . . . . 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 3258 . . . . . . . . . . 11  |-  ( ( a  i^i  x )  e.  _V  ->  ( [. ( a  i^i  x
)  /  b ]. y  e.  b  <->  y  e.  ( a  i^i  x
) ) )
362, 35e0a 31510 . . . . . . . . . 10  |-  ( [. ( a  i^i  x
)  /  b ]. y  e.  b  <->  y  e.  ( a  i^i  x
) )
37 sbceqg 3682 . . . . . . . . . . . 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 31510 . . . . . . . . . . 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 3718 . . . . . . . . . . . . . 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 31510 . . . . . . . . . . . . 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 3705 . . . . . . . . . . . . . . 15  |-  ( ( a  i^i  x )  e.  _V  ->  [_ (
a  i^i  x )  /  b ]_ b  =  ( a  i^i  x ) )
422, 41e0a 31510 . . . . . . . . . . . . . 14  |-  [_ (
a  i^i  x )  /  b ]_ b  =  ( a  i^i  x )
43 csbconstg 3306 . . . . . . . . . . . . . . 15  |-  ( ( a  i^i  x )  e.  _V  ->  [_ (
a  i^i  x )  /  b ]_ y  =  y )
442, 43e0a 31510 . . . . . . . . . . . . . 14  |-  [_ (
a  i^i  x )  /  b ]_ y  =  y
4542, 44ineq12i 3555 . . . . . . . . . . . . 13  |-  ( [_ ( a  i^i  x
)  /  b ]_ b  i^i  [_ ( a  i^i  x )  /  b ]_ y )  =  ( ( a  i^i  x
)  i^i  y )
4640, 45eqtri 2463 . . . . . . . . . . . 12  |-  [_ (
a  i^i  x )  /  b ]_ (
b  i^i  y )  =  ( ( a  i^i  x )  i^i  y )
47 csbconstg 3306 . . . . . . . . . . . . 13  |-  ( ( a  i^i  x )  e.  _V  ->  [_ (
a  i^i  x )  /  b ]_ (/)  =  (/) )
482, 47e0a 31510 . . . . . . . . . . . 12  |-  [_ (
a  i^i  x )  /  b ]_ (/)  =  (/)
4946, 48eqeq12i 2456 . . . . . . . . . . 11  |-  ( [_ ( a  i^i  x
)  /  b ]_ ( b  i^i  y
)  =  [_ (
a  i^i  x )  /  b ]_ (/)  <->  ( (
a  i^i  x )  i^i  y )  =  (/) )
5038, 49bitri 249 . . . . . . . . . 10  |-  ( [. ( a  i^i  x
)  /  b ]. ( b  i^i  y
)  =  (/)  <->  ( (
a  i^i  x )  i^i  y )  =  (/) )
5136, 50anbi12i 697 . . . . . . . . 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 249 . . . . . . . 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 1591 . . . . . . 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 1633 . . . . . . 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 31510 . . . . . 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 2726 . . . . . 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 252 . . . . 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 251 . . . 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 249 . . 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 326 . 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 249 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 184    /\ wa 369   A.wal 1367    = wceq 1369   E.wex 1586    e. wcel 1756    =/= wne 2611   E.wrex 2721   _Vcvv 2977   [.wsbc 3191   [_csb 3293    i^i cin 3332    C_ wss 3333   (/)c0 3642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-rex 2726  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-in 3340  df-ss 3347
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator