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

Theorem trintALTVD 28167
Description: The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 28168. 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 28168 is trintALTVD 28167 without virtual deductions and was automatically derived from trintALTVD 28167.
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 27885 . . . . . . 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 27903 . . . . . 6  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  z  e.  y ).
4 idn3 27887 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A ) ,. q  e.  A  ->.  q  e.  A ).
5 idn1 27836 . . . . . . . . . . . 12  |-  (. A. x  e.  A  Tr  x 
->.  A. x  e.  A  Tr  x ).
6 rspsbc 3103 . . . . . . . . . . . 12  |-  ( q  e.  A  ->  ( A. x  e.  A  Tr  x  ->  [. q  /  x ]. Tr  x
) )
74, 5, 6e31 28035 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A ) ,. q  e.  A  ->.  [. q  /  x ]. Tr  x ).
8 trsbc 27798 . . . . . . . . . . . 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 28018 . . . . . . . . . 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 27903 . . . . . . . . . . . . 13  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  y  e.  |^| A ).
13 elintg 3907 . . . . . . . . . . . . . 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 27903 . . . . . . . . . . . 12  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  A. q  e.  A  y  e.  q ).
16 rsp 2637 . . . . . . . . . . . 12  |-  ( A. q  e.  A  y  e.  q  ->  ( q  e.  A  ->  y  e.  q ) )
1715, 16e2 27903 . . . . . . . . . . 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 28042 . . . . . . . . . 10  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A ) ,. q  e.  A  ->.  y  e.  q ).
20 trel 4157 . . . . . . . . . . 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 28050 . . . . . . . . 9  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A ) ,. q  e.  A  ->.  z  e.  q ).
2322in3 27881 . . . . . . . 8  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  ( q  e.  A  ->  z  e.  q ) ).
2423gen21 27891 . . . . . . 7  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  A. q
( q  e.  A  ->  z  e.  q ) ).
25 df-ral 2582 . . . . . . . 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 27903 . . . . . 6  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  A. q  e.  A  z  e.  q ).
28 elintg 3907 . . . . . . 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 27943 . . . . 5  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  z  e.  |^| A ).
3130in2 27877 . . . 4  |-  (. A. x  e.  A  Tr  x 
->.  ( ( z  e.  y  /\  y  e. 
|^| A )  -> 
z  e.  |^| A
) ).
3231gen12 27890 . . 3  |-  (. A. x  e.  A  Tr  x 
->.  A. z A. y
( ( z  e.  y  /\  y  e. 
|^| A )  -> 
z  e.  |^| A
) ).
33 dftr2 4152 . . . 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_ 27899 . 2  |-  (. A. x  e.  A  Tr  x 
->.  Tr  |^| A ).
3635in1 27833 1  |-  ( A. x  e.  A  Tr  x  ->  Tr  |^| A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1531    e. wcel 1701   A.wral 2577   [.wsbc 3025   |^|cint 3899   Tr wtr 4150
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ral 2582  df-v 2824  df-sbc 3026  df-in 3193  df-ss 3200  df-uni 3865  df-int 3900  df-tr 4151  df-vd1 27832  df-vd2 27841  df-vd3 27853
  Copyright terms: Public domain W3C validator