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

Theorem truniALT 28604
Description: The union of a class of transitive sets is transitive. Alternate proof of truni 4143. truniALT 28604 is truniALTVD 28970 without virtual deductions and was automatically derived from truniALTVD 28970 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
truniALT  |-  ( A. x  e.  A  Tr  x  ->  Tr  U. A )
Distinct variable group:    x, A

Proof of Theorem truniALT
Dummy variables  q 
y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 447 . . . . . 6  |-  ( ( z  e.  y  /\  y  e.  U. A )  ->  y  e.  U. A )
21a1i 10 . . . . 5  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
y  e.  U. A
) )
3 eluni 3846 . . . . 5  |-  ( y  e.  U. A  <->  E. q
( y  e.  q  /\  q  e.  A
) )
42, 3syl6ib 217 . . . 4  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  ->  E. q ( y  e.  q  /\  q  e.  A ) ) )
5 simpl 443 . . . . . . . . 9  |-  ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  y )
65a1i 10 . . . . . . . 8  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
z  e.  y ) )
7 simpl 443 . . . . . . . . 9  |-  ( ( y  e.  q  /\  q  e.  A )  ->  y  e.  q )
87a1ii 24 . . . . . . . 8  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
( ( y  e.  q  /\  q  e.  A )  ->  y  e.  q ) ) )
9 simpr 447 . . . . . . . . . 10  |-  ( ( y  e.  q  /\  q  e.  A )  ->  q  e.  A )
109a1ii 24 . . . . . . . . 9  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
( ( y  e.  q  /\  q  e.  A )  ->  q  e.  A ) ) )
11 rspsbc 3082 . . . . . . . . . . 11  |-  ( q  e.  A  ->  ( A. x  e.  A  Tr  x  ->  [. q  /  x ]. Tr  x
) )
1211com12 27 . . . . . . . . . 10  |-  ( A. x  e.  A  Tr  x  ->  ( q  e.  A  ->  [. q  /  x ]. Tr  x ) )
1310, 12syl6d 64 . . . . . . . . 9  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
( ( y  e.  q  /\  q  e.  A )  ->  [. q  /  x ]. Tr  x
) ) )
14 trsbc 28603 . . . . . . . . . 10  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  <->  Tr  q
) )
1514biimpd 198 . . . . . . . . 9  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  ->  Tr  q ) )
1610, 13, 15ee33 28583 . . . . . . . 8  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
( ( y  e.  q  /\  q  e.  A )  ->  Tr  q ) ) )
17 trel 4136 . . . . . . . . 9  |-  ( Tr  q  ->  ( (
z  e.  y  /\  y  e.  q )  ->  z  e.  q ) )
1817exp3acom3r 1360 . . . . . . . 8  |-  ( z  e.  y  ->  (
y  e.  q  -> 
( Tr  q  -> 
z  e.  q ) ) )
196, 8, 16, 18ee233 28580 . . . . . . 7  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
( ( y  e.  q  /\  q  e.  A )  ->  z  e.  q ) ) )
20 elunii 3848 . . . . . . . 8  |-  ( ( z  e.  q  /\  q  e.  A )  ->  z  e.  U. A
)
2120ex 423 . . . . . . 7  |-  ( z  e.  q  ->  (
q  e.  A  -> 
z  e.  U. A
) )
2219, 10, 21ee33 28583 . . . . . 6  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
( ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A ) ) )
2322alrimdv 1623 . . . . 5  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  ->  A. q ( ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A ) ) )
24 19.23v 1844 . . . . 5  |-  ( A. q ( ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A )  <->  ( E. q ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A ) )
2523, 24syl6ib 217 . . . 4  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
( E. q ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A
) ) )
264, 25mpdd 36 . . 3  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
z  e.  U. A
) )
2726alrimivv 1622 . 2  |-  ( A. x  e.  A  Tr  x  ->  A. z A. y
( ( z  e.  y  /\  y  e. 
U. A )  -> 
z  e.  U. A
) )
28 dftr2 4131 . 2  |-  ( Tr 
U. A  <->  A. z A. y ( ( z  e.  y  /\  y  e.  U. A )  -> 
z  e.  U. A
) )
2927, 28sylibr 203 1  |-  ( A. x  e.  A  Tr  x  ->  Tr  U. A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1530   E.wex 1531    e. wcel 1696   A.wral 2556   [.wsbc 3004   U.cuni 3843   Tr wtr 4129
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803  df-sbc 3005  df-in 3172  df-ss 3179  df-uni 3844  df-tr 4130
  Copyright terms: Public domain W3C validator