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

Theorem trintALTVD 28656
Description: The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 28657. 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. trintALT 28657 is trintALTVD 28656 without virtual deductions and was automatically derived from trintALTVD 28656.
1::  |-  (. A. x  e.  A Tr  x  ->.  A. x  e.  A Tr  x ).
2::  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  ( z  e.  y  /\  y  e.  |^| A ) ).
3:2:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  z  e.  y ).
4:2:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  y  e.  |^| A ).
5:4:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  A. q  e.  A y  e.  q ).
6:5:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  ( q  e.  A  ->  y  e.  q ) ).
7::  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  q  e.  A ).
8:7,6:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  y  e.  q ).
9:7,1:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  [ q  /  x ] Tr  x ).
10:7,9:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  Tr  q ).
11:10,3,8:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A ) ,  q  e.  A  ->.  z  e.  q ).
12:11:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  ( q  e.  A  ->  z  e.  q ) ).
13:12:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  A. q ( q  e.  A  ->  z  e.  q ) ).
14:13:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  A. q  e.  A z  e.  q ).
15:3,14:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  |^| A )  ->.  z  e.  |^| A ).
16:15:  |-  (. A. x  e.  A Tr  x  ->.  ( ( z  e.  y  /\  y  e.  |^| A )  ->  z  e.  |^| A ) ).
17:16:  |-  (. A. x  e.  A Tr  x  ->.  A. z A. y ( ( z  e.  y  /\  y  e.  |^| A )  ->  z  e.  |^| A ) ).
18:17:  |-  (. A. x  e.  A Tr  x  ->.  Tr  |^| A ).
qed:18:  |-  ( A. x  e.  A Tr  x  ->  Tr  |^| A )
(Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
trintALTVD  |-  ( A. x  e.  A  Tr  x  ->  Tr  |^| A )
Distinct variable group:    x, A

Proof of Theorem trintALTVD
Dummy variables  q 
y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn2 28385 . . . . . . 7  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  ( z  e.  y  /\  y  e.  |^| A ) ).
2 simpl 443 . . . . . . 7  |-  ( ( z  e.  y  /\  y  e.  |^| A )  ->  z  e.  y )
31, 2e2 28403 . . . . . 6  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  z  e.  y ).
4 idn3 28387 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A ) ,. q  e.  A  ->.  q  e.  A ).
5 idn1 28342 . . . . . . . . . . . 12  |-  (. A. x  e.  A  Tr  x 
->.  A. x  e.  A  Tr  x ).
6 rspsbc 3069 . . . . . . . . . . . 12  |-  ( q  e.  A  ->  ( A. x  e.  A  Tr  x  ->  [. q  /  x ]. Tr  x
) )
74, 5, 6e31 28526 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A ) ,. q  e.  A  ->.  [. q  /  x ]. Tr  x ).
8 trsbc 28304 . . . . . . . . . . . 12  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  <->  Tr  q
) )
98biimpd 198 . . . . . . . . . . 11  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  ->  Tr  q ) )
104, 7, 9e33 28509 . . . . . . . . . 10  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A ) ,. q  e.  A  ->.  Tr  q ).
11 simpr 447 . . . . . . . . . . . . . 14  |-  ( ( z  e.  y  /\  y  e.  |^| A )  ->  y  e.  |^| A )
121, 11e2 28403 . . . . . . . . . . . . 13  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  y  e.  |^| A ).
13 elintg 3870 . . . . . . . . . . . . . 14  |-  ( y  e.  |^| A  ->  (
y  e.  |^| A  <->  A. q  e.  A  y  e.  q ) )
1413ibi 232 . . . . . . . . . . . . 13  |-  ( y  e.  |^| A  ->  A. q  e.  A  y  e.  q )
1512, 14e2 28403 . . . . . . . . . . . 12  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  A. q  e.  A  y  e.  q ).
16 rsp 2603 . . . . . . . . . . . 12  |-  ( A. q  e.  A  y  e.  q  ->  ( q  e.  A  ->  y  e.  q ) )
1715, 16e2 28403 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  ( q  e.  A  ->  y  e.  q ) ).
18 pm2.27 35 . . . . . . . . . . 11  |-  ( q  e.  A  ->  (
( q  e.  A  ->  y  e.  q )  ->  y  e.  q ) )
194, 17, 18e32 28533 . . . . . . . . . 10  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A ) ,. q  e.  A  ->.  y  e.  q ).
20 trel 4120 . . . . . . . . . . 11  |-  ( Tr  q  ->  ( (
z  e.  y  /\  y  e.  q )  ->  z  e.  q ) )
2120exp3a 425 . . . . . . . . . 10  |-  ( Tr  q  ->  ( z  e.  y  ->  ( y  e.  q  ->  z  e.  q ) ) )
2210, 3, 19, 21e323 28541 . . . . . . . . 9  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A ) ,. q  e.  A  ->.  z  e.  q ).
2322in3 28381 . . . . . . . 8  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  ( q  e.  A  ->  z  e.  q ) ).
2423gen21 28391 . . . . . . 7  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  A. q
( q  e.  A  ->  z  e.  q ) ).
25 df-ral 2548 . . . . . . . 8  |-  ( A. q  e.  A  z  e.  q  <->  A. q ( q  e.  A  ->  z  e.  q ) )
2625biimpri 197 . . . . . . 7  |-  ( A. q ( q  e.  A  ->  z  e.  q )  ->  A. q  e.  A  z  e.  q )
2724, 26e2 28403 . . . . . 6  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  A. q  e.  A  z  e.  q ).
28 elintg 3870 . . . . . . 7  |-  ( z  e.  y  ->  (
z  e.  |^| A  <->  A. q  e.  A  z  e.  q ) )
2928biimprd 214 . . . . . 6  |-  ( z  e.  y  ->  ( A. q  e.  A  z  e.  q  ->  z  e.  |^| A ) )
303, 27, 29e22 28443 . . . . 5  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  z  e.  |^| A ).
3130in2 28377 . . . 4  |-  (. A. x  e.  A  Tr  x 
->.  ( ( z  e.  y  /\  y  e. 
|^| A )  -> 
z  e.  |^| A
) ).
3231gen12 28390 . . 3  |-  (. A. x  e.  A  Tr  x 
->.  A. z A. y
( ( z  e.  y  /\  y  e. 
|^| A )  -> 
z  e.  |^| A
) ).
33 dftr2 4115 . . . 4  |-  ( Tr 
|^| A  <->  A. z A. y ( ( z  e.  y  /\  y  e.  |^| A )  -> 
z  e.  |^| A
) )
3433biimpri 197 . . 3  |-  ( A. z A. y ( ( z  e.  y  /\  y  e.  |^| A )  ->  z  e.  |^| A )  ->  Tr  |^| A )
3532, 34e1_ 28399 . 2  |-  (. A. x  e.  A  Tr  x 
->.  Tr  |^| A ).
3635in1 28339 1  |-  ( A. x  e.  A  Tr  x  ->  Tr  |^| A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1527    e. wcel 1684   A.wral 2543   [.wsbc 2991   |^|cint 3862   Tr wtr 4113
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-or 359  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-nfc 2408  df-ral 2548  df-v 2790  df-sbc 2992  df-in 3159  df-ss 3166  df-uni 3828  df-int 3863  df-tr 4114  df-vd1 28338  df-vd2 28347  df-vd3 28359
  Copyright terms: Public domain W3C validator