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

Theorem onfrALTlem1VD 28411
Description: Virtual deduction proof of onfrALTlem1 28041. 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. onfrALTlem1 28041 is onfrALTlem1VD 28411 without virtual deductions and was automatically derived from onfrALTlem1VD 28411.
1::  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ->.  ( x  e.  a  /\  ( a  i^i  x )  =  (/) ) ).
2:1:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ->.  E. x ( x  e.  a  /\  ( a  i^i  x )  =  (/) ) ).
3:2:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ->.  E. y [ y  /  x ] ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ).
4::  |-  ( [ y  /  x ] ( x  e.  a  /\  ( a  i^i  x )  =  (/)  )  <->  ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) )
5:4:  |-  A. y ( [ y  /  x ] ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  <->  ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) )
6:5:  |-  ( E. y [ y  /  x ] ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  <->  E. y ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) )
7:3,6:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ->.  E. y ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) ).
8::  |-  ( E. y  e.  a ( a  i^i  y )  =  (/)  <->  E. y (  y  e.  a  /\  ( a  i^i  y )  =  (/) ) )
qed:7,8:  |-  (. ( a  C_  On  /\  a  =/=  (/) ) ,. ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ->.  E. y  e.  a ( a  i^i  y )  =  (/) ).
(Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
onfrALTlem1VD  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  ( a  i^i  x
)  =  (/) )  ->.  E. y  e.  a  ( a  i^i  y )  =  (/) ).
Distinct variable group:    x, a, y

Proof of Theorem onfrALTlem1VD
StepHypRef Expression
1 idn2 28119 . . . . 5  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  ( a  i^i  x
)  =  (/) )  ->.  ( x  e.  a  /\  (
a  i^i  x )  =  (/) ) ).
2 19.8a 1747 . . . . 5  |-  ( ( x  e.  a  /\  ( a  i^i  x
)  =  (/) )  ->  E. x ( x  e.  a  /\  ( a  i^i  x )  =  (/) ) )
31, 2e2 28137 . . . 4  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  ( a  i^i  x
)  =  (/) )  ->.  E. x
( x  e.  a  /\  ( a  i^i  x )  =  (/) ) ).
4 cbvexsv 28040 . . . . 5  |-  ( E. x ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  <->  E. y [ y  /  x ] ( x  e.  a  /\  ( a  i^i  x
)  =  (/) ) )
54biimpi 186 . . . 4  |-  ( E. x ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  ->  E. y [ y  /  x ] ( x  e.  a  /\  ( a  i^i  x )  =  (/) ) )
63, 5e2 28137 . . 3  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  ( a  i^i  x
)  =  (/) )  ->.  E. y [ y  /  x ] ( x  e.  a  /\  ( a  i^i  x )  =  (/) ) ).
7 sbsbc 3071 . . . . . 6  |-  ( [ y  /  x ]
( x  e.  a  /\  ( a  i^i  x )  =  (/) ) 
<-> 
[. y  /  x ]. ( x  e.  a  /\  ( a  i^i  x )  =  (/) ) )
8 onfrALTlem4 28036 . . . . . 6  |-  ( [. y  /  x ]. (
x  e.  a  /\  ( a  i^i  x
)  =  (/) )  <->  ( y  e.  a  /\  (
a  i^i  y )  =  (/) ) )
97, 8bitri 240 . . . . 5  |-  ( [ y  /  x ]
( x  e.  a  /\  ( a  i^i  x )  =  (/) ) 
<->  ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) )
109ax-gen 1546 . . . 4  |-  A. y
( [ y  /  x ] ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  <->  ( y  e.  a  /\  ( a  i^i  y )  =  (/) ) )
11 exbi 1581 . . . 4  |-  ( A. y ( [ y  /  x ] ( x  e.  a  /\  ( a  i^i  x
)  =  (/) )  <->  ( y  e.  a  /\  (
a  i^i  y )  =  (/) ) )  -> 
( E. y [ y  /  x ]
( x  e.  a  /\  ( a  i^i  x )  =  (/) ) 
<->  E. y ( y  e.  a  /\  (
a  i^i  y )  =  (/) ) ) )
1210, 11e0_ 28290 . . 3  |-  ( E. y [ y  /  x ] ( x  e.  a  /\  ( a  i^i  x )  =  (/) )  <->  E. y ( y  e.  a  /\  (
a  i^i  y )  =  (/) ) )
136, 12e2bi 28138 . 2  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  ( a  i^i  x
)  =  (/) )  ->.  E. y
( y  e.  a  /\  ( a  i^i  y )  =  (/) ) ).
14 df-rex 2625 . 2  |-  ( E. y  e.  a  ( a  i^i  y )  =  (/)  <->  E. y ( y  e.  a  /\  (
a  i^i  y )  =  (/) ) )
1513, 14e2bir 28139 1  |-  (. (
a  C_  On  /\  a  =/=  (/) ) ,. (
x  e.  a  /\  ( a  i^i  x
)  =  (/) )  ->.  E. y  e.  a  ( a  i^i  y )  =  (/) ).
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   A.wal 1540   E.wex 1541    = wceq 1642   [wsb 1648    e. wcel 1710    =/= wne 2521   E.wrex 2620   [.wsbc 3067    i^i cin 3227    C_ wss 3228   (/)c0 3531   Oncon0 4471   (.wvd2 28074
This theorem is referenced by:  onfrALTVD  28412
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-in 3235  df-vd2 28075
  Copyright terms: Public domain W3C validator