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

Theorem truniALT 28305
Description: The union of a class of transitive sets is transitive. Alternate proof of truni 4127. truniALT 28305 is truniALTVD 28654 without virtual deductions and was automatically derived from truniALTVD 28654 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 3830 . . . . 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 3069 . . . . . . . . . . 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 28304 . . . . . . . . . 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 28284 . . . . . . . 8  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
( ( y  e.  q  /\  q  e.  A )  ->  Tr  q ) ) )
17 trel 4120 . . . . . . . . 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 28281 . . . . . . 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 3832 . . . . . . . 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 28284 . . . . . 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 1619 . . . . 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 1832 . . . . 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 1618 . 2  |-  ( A. x  e.  A  Tr  x  ->  A. z A. y
( ( z  e.  y  /\  y  e. 
U. A )  -> 
z  e.  U. A
) )
28 dftr2 4115 . 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 1527   E.wex 1528    e. wcel 1684   A.wral 2543   [.wsbc 2991   U.cuni 3827   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-tr 4114
  Copyright terms: Public domain W3C validator