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

Theorem trintALTVD 28929
Description: The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 28930. 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 28930 is trintALTVD 28929 without virtual deductions and was automatically derived from trintALTVD 28929.
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 28651 . . . . . . 7  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  ( z  e.  y  /\  y  e.  |^| A ) ).
2 simpl 444 . . . . . . 7  |-  ( ( z  e.  y  /\  y  e.  |^| A )  ->  z  e.  y )
31, 2e2 28669 . . . . . 6  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  z  e.  y ).
4 idn3 28653 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A ) ,. q  e.  A  ->.  q  e.  A ).
5 idn1 28602 . . . . . . . . . . . 12  |-  (. A. x  e.  A  Tr  x 
->.  A. x  e.  A  Tr  x ).
6 rspsbc 3231 . . . . . . . . . . . 12  |-  ( q  e.  A  ->  ( A. x  e.  A  Tr  x  ->  [. q  /  x ]. Tr  x
) )
74, 5, 6e31 28800 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A ) ,. q  e.  A  ->.  [. q  /  x ]. Tr  x ).
8 trsbc 28562 . . . . . . . . . . . 12  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  <->  Tr  q
) )
98biimpd 199 . . . . . . . . . . 11  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  ->  Tr  q ) )
104, 7, 9e33 28783 . . . . . . . . . 10  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A ) ,. q  e.  A  ->.  Tr  q ).
11 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( z  e.  y  /\  y  e.  |^| A )  ->  y  e.  |^| A )
121, 11e2 28669 . . . . . . . . . . . . 13  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  y  e.  |^| A ).
13 elintg 4050 . . . . . . . . . . . . . 14  |-  ( y  e.  |^| A  ->  (
y  e.  |^| A  <->  A. q  e.  A  y  e.  q ) )
1413ibi 233 . . . . . . . . . . . . 13  |-  ( y  e.  |^| A  ->  A. q  e.  A  y  e.  q )
1512, 14e2 28669 . . . . . . . . . . . 12  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  A. q  e.  A  y  e.  q ).
16 rsp 2758 . . . . . . . . . . . 12  |-  ( A. q  e.  A  y  e.  q  ->  ( q  e.  A  ->  y  e.  q ) )
1715, 16e2 28669 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  ( q  e.  A  ->  y  e.  q ) ).
18 pm2.27 37 . . . . . . . . . . 11  |-  ( q  e.  A  ->  (
( q  e.  A  ->  y  e.  q )  ->  y  e.  q ) )
194, 17, 18e32 28807 . . . . . . . . . 10  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A ) ,. q  e.  A  ->.  y  e.  q ).
20 trel 4301 . . . . . . . . . . 11  |-  ( Tr  q  ->  ( (
z  e.  y  /\  y  e.  q )  ->  z  e.  q ) )
2120exp3a 426 . . . . . . . . . 10  |-  ( Tr  q  ->  ( z  e.  y  ->  ( y  e.  q  ->  z  e.  q ) ) )
2210, 3, 19, 21e323 28815 . . . . . . . . 9  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A ) ,. q  e.  A  ->.  z  e.  q ).
2322in3 28647 . . . . . . . 8  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  ( q  e.  A  ->  z  e.  q ) ).
2423gen21 28657 . . . . . . 7  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  A. q
( q  e.  A  ->  z  e.  q ) ).
25 df-ral 2702 . . . . . . . 8  |-  ( A. q  e.  A  z  e.  q  <->  A. q ( q  e.  A  ->  z  e.  q ) )
2625biimpri 198 . . . . . . 7  |-  ( A. q ( q  e.  A  ->  z  e.  q )  ->  A. q  e.  A  z  e.  q )
2724, 26e2 28669 . . . . . 6  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  A. q  e.  A  z  e.  q ).
28 elintg 4050 . . . . . . 7  |-  ( z  e.  y  ->  (
z  e.  |^| A  <->  A. q  e.  A  z  e.  q ) )
2928biimprd 215 . . . . . 6  |-  ( z  e.  y  ->  ( A. q  e.  A  z  e.  q  ->  z  e.  |^| A ) )
303, 27, 29e22 28709 . . . . 5  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
|^| A )  ->.  z  e.  |^| A ).
3130in2 28643 . . . 4  |-  (. A. x  e.  A  Tr  x 
->.  ( ( z  e.  y  /\  y  e. 
|^| A )  -> 
z  e.  |^| A
) ).
3231gen12 28656 . . 3  |-  (. A. x  e.  A  Tr  x 
->.  A. z A. y
( ( z  e.  y  /\  y  e. 
|^| A )  -> 
z  e.  |^| A
) ).
33 dftr2 4296 . . . 4  |-  ( Tr 
|^| A  <->  A. z A. y ( ( z  e.  y  /\  y  e.  |^| A )  -> 
z  e.  |^| A
) )
3433biimpri 198 . . 3  |-  ( A. z A. y ( ( z  e.  y  /\  y  e.  |^| A )  ->  z  e.  |^| A )  ->  Tr  |^| A )
3532, 34e1_ 28665 . 2  |-  (. A. x  e.  A  Tr  x 
->.  Tr  |^| A ).
3635in1 28599 1  |-  ( A. x  e.  A  Tr  x  ->  Tr  |^| A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1549    e. wcel 1725   A.wral 2697   [.wsbc 3153   |^|cint 4042   Tr wtr 4294
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-v 2950  df-sbc 3154  df-in 3319  df-ss 3326  df-uni 4008  df-int 4043  df-tr 4295  df-vd1 28598  df-vd2 28607  df-vd3 28619
  Copyright terms: Public domain W3C validator