Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ssralv2VD Structured version   Visualization version   Unicode version
Theorem ssralv2VD 39102
Description: Quantification restricted to a subclass for two quantifiers. ssralv 3666 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 38737 is ssralv2VD 39102 without virtual deductions and was automatically derived from ssralv2VD 39102.
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 1839 . . . . 5 |- ( ( A C_ B /\ C C_ D ) -> A. x ( A C_ B /\ C C_ D ) )
2 hbra1 2942 . . . . 5 |- ( A. x e. B A. y e. D ph -> A. x A. x e. B A. y e. D ph )
3 idn1 38790 . . . . . . . 8 |- (. ( A C_ B /\ C C_ D ) ->. ( A C_ B /\ C C_ D ) ).
4 simpr 477 . . . . . . . 8 |- ( ( A C_ B /\ C C_ D ) -> C C_ D )
53, 4e1a 38852 . . . . . . 7 |- (. ( A C_ B /\ C C_ D ) ->. C C_ D ).
6 idn3 38840 . . . . . . . 8 |- (. ( A C_ B /\ C C_ D ) ,. A. x e. B A. y e. D ph ,. x e. A ->. x e. A ).
7 simpl 473 . . . . . . . . . . . 12 |- ( ( A C_ B /\ C C_ D ) -> A C_ B )
83, 7e1a 38852 . . . . . . . . . . 11 |- (. ( A C_ B /\ C C_ D ) ->. A C_ B ).
9 idn2 38838 . . . . . . . . . . 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 3666 . . . . . . . . . . 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 38951 . . . . . . . . . 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 2917 . . . . . . . . . . 11 |- ( A. x e. A A. y e. D ph <-> A. x ( x e. A -> A. y e. D ph ) )
1312biimpi 206 . . . . . . . . . 10 |- ( A. x e. A A. y e. D ph -> A. x ( x e. A -> A. y e. D ph ) )
1411, 13e2 38856 . . . . . . . . 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 2053 . . . . . . . . 9 |- ( A. x ( x e. A -> A. y e. D ph ) -> ( x e. A -> A. y e. D ph ) )
1614, 15e2 38856 . . . . . . . 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 42 . . . . . . . 8 |- ( x e. A -> ( ( x e. A -> A. y e. D ph ) -> A. y e. D ph ) )
186, 16, 17e32 38985 . . . . . . 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 3666 . . . . . . 7 |- ( C C_ D -> ( A. y e. D ph -> A. y e. C ph ) )
205, 18, 19e13 38975 . . . . . 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 38834 . . . . 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 38845 . . . 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 2917 . . . . 5 |- ( A. x e. A A. y e. C ph <-> A. x ( x e. A -> A. y e. C ph ) )
2423biimpri 218 . . . 4 |- ( A. x ( x e. A -> A. y e. C ph ) -> A. x e. A A. y e. C ph )
2522, 24e2 38856 . . 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 38830 . 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 38787 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 384   A.wal 1481   e. wcel 1990   A.wral 2912   C_ wss 3574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-in 3581  df-ss 3588  df-vd1 38786  df-vd2 38794  df-vd3 38806
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator