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

Theorem ssralv2VD 34067
Description: Quantification restricted to a subclass for two quantifiers. ssralv 3550 for two quantifiers. 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. ssralv2 33688 is ssralv2VD 34067 without virtual deductions and was automatically derived from ssralv2VD 34067.
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-5 1709 . . . . 5  |-  ( ( A  C_  B  /\  C  C_  D )  ->  A. x ( A  C_  B  /\  C  C_  D
) )
2 hbra1 2836 . . . . 5  |-  ( A. x  e.  B  A. y  e.  D  ph  ->  A. x A. x  e.  B  A. y  e.  D  ph )
3 idn1 33745 . . . . . . . 8  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  ( A  C_  B  /\  C  C_  D ) ).
4 simpr 459 . . . . . . . 8  |-  ( ( A  C_  B  /\  C  C_  D )  ->  C  C_  D )
53, 4e1a 33807 . . . . . . 7  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  C  C_  D ).
6 idn3 33795 . . . . . . . 8  |-  (. ( A  C_  B  /\  C  C_  D ) ,. A. x  e.  B  A. y  e.  D  ph ,. x  e.  A  ->.  x  e.  A ).
7 simpl 455 . . . . . . . . . . . 12  |-  ( ( A  C_  B  /\  C  C_  D )  ->  A  C_  B )
83, 7e1a 33807 . . . . . . . . . . 11  |-  (. ( A  C_  B  /\  C  C_  D )  ->.  A  C_  B ).
9 idn2 33793 . . . . . . . . . . 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 3550 . . . . . . . . . . 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 33915 . . . . . . . . . 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 2809 . . . . . . . . . . 11  |-  ( A. x  e.  A  A. y  e.  D  ph  <->  A. x
( x  e.  A  ->  A. y  e.  D  ph ) )
1312biimpi 194 . . . . . . . . . 10  |-  ( A. x  e.  A  A. y  e.  D  ph  ->  A. x ( x  e.  A  ->  A. y  e.  D  ph ) )
1411, 13e2 33811 . . . . . . . . 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 1864 . . . . . . . . 9  |-  ( A. x ( x  e.  A  ->  A. y  e.  D  ph )  -> 
( x  e.  A  ->  A. y  e.  D  ph ) )
1614, 15e2 33811 . . . . . . . 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 39 . . . . . . . 8  |-  ( x  e.  A  ->  (
( x  e.  A  ->  A. y  e.  D  ph )  ->  A. y  e.  D  ph ) )
186, 16, 17e32 33949 . . . . . . 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 3550 . . . . . . 7  |-  ( C 
C_  D  ->  ( A. y  e.  D  ph 
->  A. y  e.  C  ph ) )
205, 18, 19e13 33939 . . . . . 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 33789 . . . . 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 33800 . . . 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 2809 . . . . 5  |-  ( A. x  e.  A  A. y  e.  C  ph  <->  A. x
( x  e.  A  ->  A. y  e.  C  ph ) )
2423biimpri 206 . . . 4  |-  ( A. x ( x  e.  A  ->  A. y  e.  C  ph )  ->  A. x  e.  A  A. y  e.  C  ph )
2522, 24e2 33811 . . 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 33785 . 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 33742 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 setvar class
Syntax hints:    -> wi 4    /\ wa 367   A.wal 1396    e. wcel 1823   A.wral 2804    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2809  df-in 3468  df-ss 3475  df-vd1 33741  df-vd2 33749  df-vd3 33761
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator