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

Theorem ssralv2VD 28642
Description: Quantification restricted to a subclass for two quantifiers. ssralv 3237 for two quantifiers. 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. ssralv2 28294 is ssralv2VD 28642 without virtual deductions and was automatically derived from ssralv2VD 28642.
1::  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  ( A  C_  B  /\  C  C_  D ) ).
2::  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x  e.  B A. y  e.  D ph ).
3:1:  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  A  C_  B ).
4:3,2:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x  e.  A A. y  e.  D ph ).
5:4:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x ( x  e.  A  ->  A. y  e.  D ph ) ).
6:5:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  ( x  e.  A  ->  A. y  e.  D ph ) ).
7::  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph ,  x  e.  A  ->.  x  e.  A ).
8:7,6:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph ,  x  e.  A  ->.  A. y  e.  D ph ).
9:1:  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  C  C_  D ).
10:9,8:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph ,  x  e.  A  ->.  A. y  e.  C ph ).
11:10:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  ( x  e.  A  ->  A. y  e.  C ph ) ).
12::  |-  ( ( A  C_  B  /\  C  C_  D )  ->  A. x ( A  C_  B  /\  C  C_  D ) )
13::  |-  ( A. x  e.  B A. y  e.  D ph  ->  A. x A. x  e.  B A. y  e.  D ph )
14:12,13,11:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x ( x  e.  A  ->  A. y  e.  C ph ) ).
15:14:  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D ph  ->.  A. x  e.  A A. y  e.  C ph ).
16:15:  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  ( A. x  e.  B A. y  e.  D ph  ->  A. x  e.  A A. y  e.  C ph ) ).
qed:16:  |-  ( ( A  C_  B  /\  C  C_  D )  ->  ( A. x  e.  B A. y  e.  D ph  ->  A. x  e.  A A. y  e.  C ph ) )
(Contributed by Alan Sare, 10-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ssralv2VD  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A. x  e.  B  A. y  e.  D  ph  ->  A. x  e.  A  A. y  e.  C  ph ) )
Distinct variable groups:    x, A    x, B    x, C    y, C    x, D    y, D
Allowed substitution hints:    ph( x, y)    A( y)    B( y)

Proof of Theorem ssralv2VD
StepHypRef Expression
1 ax-17 1603 . . . . 5  |-  ( ( A  C_  B  /\  C  C_  D )  ->  A. x ( A  C_  B  /\  C  C_  D
) )
2 hbra1 2592 . . . . 5  |-  ( A. x  e.  B  A. y  e.  D  ph  ->  A. x A. x  e.  B  A. y  e.  D  ph )
3 idn1 28342 . . . . . . . 8  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  ( A  C_  B  /\  C  C_  D ) ).
4 simpr 447 . . . . . . . 8  |-  ( ( A  C_  B  /\  C  C_  D )  ->  C  C_  D )
53, 4e1_ 28399 . . . . . . 7  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  C  C_  D ).
6 idn3 28387 . . . . . . . 8  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph ,. x  e.  A  ->.  x  e.  A ).
7 simpl 443 . . . . . . . . . . . 12  |-  ( ( A  C_  B  /\  C  C_  D )  ->  A  C_  B )
83, 7e1_ 28399 . . . . . . . . . . 11  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  A  C_  B ).
9 idn2 28385 . . . . . . . . . . 11  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph  ->.  A. x  e.  B  A. y  e.  D  ph ).
10 ssralv 3237 . . . . . . . . . . 11  |-  ( A 
C_  B  ->  ( A. x  e.  B  A. y  e.  D  ph 
->  A. x  e.  A  A. y  e.  D  ph ) )
118, 9, 10e12 28499 . . . . . . . . . 10  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph  ->.  A. x  e.  A  A. y  e.  D  ph ).
12 df-ral 2548 . . . . . . . . . . 11  |-  ( A. x  e.  A  A. y  e.  D  ph  <->  A. x
( x  e.  A  ->  A. y  e.  D  ph ) )
1312biimpi 186 . . . . . . . . . 10  |-  ( A. x  e.  A  A. y  e.  D  ph  ->  A. x ( x  e.  A  ->  A. y  e.  D  ph ) )
1411, 13e2 28403 . . . . . . . . 9  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph  ->.  A. x
( x  e.  A  ->  A. y  e.  D  ph ) ).
15 sp 1716 . . . . . . . . 9  |-  ( A. x ( x  e.  A  ->  A. y  e.  D  ph )  -> 
( x  e.  A  ->  A. y  e.  D  ph ) )
1614, 15e2 28403 . . . . . . . 8  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph  ->.  ( x  e.  A  ->  A. y  e.  D  ph ) ).
17 pm2.27 35 . . . . . . . 8  |-  ( x  e.  A  ->  (
( x  e.  A  ->  A. y  e.  D  ph )  ->  A. y  e.  D  ph ) )
186, 16, 17e32 28533 . . . . . . 7  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph ,. x  e.  A  ->.  A. y  e.  D  ph ).
19 ssralv 3237 . . . . . . 7  |-  ( C 
C_  D  ->  ( A. y  e.  D  ph 
->  A. y  e.  C  ph ) )
205, 18, 19e13 28523 . . . . . 6  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph ,. x  e.  A  ->.  A. y  e.  C  ph ).
2120in3 28381 . . . . 5  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph  ->.  ( x  e.  A  ->  A. y  e.  C  ph ) ).
221, 2, 21gen21nv 28392 . . . 4  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph  ->.  A. x
( x  e.  A  ->  A. y  e.  C  ph ) ).
23 df-ral 2548 . . . . 5  |-  ( A. x  e.  A  A. y  e.  C  ph  <->  A. x
( x  e.  A  ->  A. y  e.  C  ph ) )
2423biimpri 197 . . . 4  |-  ( A. x ( x  e.  A  ->  A. y  e.  C  ph )  ->  A. x  e.  A  A. y  e.  C  ph )
2522, 24e2 28403 . . 3  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph  ->.  A. x  e.  A  A. y  e.  C  ph ).
2625in2 28377 . 2  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  ( A. x  e.  B  A. y  e.  D  ph  ->  A. x  e.  A  A. y  e.  C  ph ) ).
2726in1 28339 1  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A. x  e.  B  A. y  e.  D  ph  ->  A. x  e.  A  A. y  e.  C  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1527    e. wcel 1684   A.wral 2543    C_ wss 3152
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ral 2548  df-in 3159  df-ss 3166  df-vd1 28338  df-vd2 28347  df-vd3 28359
  Copyright terms: Public domain W3C validator