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

Theorem truniALT 28627
Description: The union of a class of transitive sets is transitive. Alternate proof of truni 4317. truniALT 28627 is truniALTVD 28991 without virtual deductions and was automatically derived from truniALTVD 28991 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 449 . . . . . 6  |-  ( ( z  e.  y  /\  y  e.  U. A )  ->  y  e.  U. A )
21a1i 11 . . . . 5  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
y  e.  U. A
) )
3 eluni 4019 . . . . 5  |-  ( y  e.  U. A  <->  E. q
( y  e.  q  /\  q  e.  A
) )
42, 3syl6ib 219 . . . 4  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  ->  E. q ( y  e.  q  /\  q  e.  A ) ) )
5 simpl 445 . . . . . . . . 9  |-  ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  y )
65a1i 11 . . . . . . . 8  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
z  e.  y ) )
7 simpl 445 . . . . . . . . 9  |-  ( ( y  e.  q  /\  q  e.  A )  ->  y  e.  q )
87a1ii 26 . . . . . . . 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 449 . . . . . . . . . 10  |-  ( ( y  e.  q  /\  q  e.  A )  ->  q  e.  A )
109a1ii 26 . . . . . . . . 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 3240 . . . . . . . . . . 11  |-  ( q  e.  A  ->  ( A. x  e.  A  Tr  x  ->  [. q  /  x ]. Tr  x
) )
1211com12 30 . . . . . . . . . 10  |-  ( A. x  e.  A  Tr  x  ->  ( q  e.  A  ->  [. q  /  x ]. Tr  x ) )
1310, 12syl6d 67 . . . . . . . . 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 28626 . . . . . . . . . 10  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  <->  Tr  q
) )
1514biimpd 200 . . . . . . . . 9  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  ->  Tr  q ) )
1610, 13, 15ee33 28606 . . . . . . . 8  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
( ( y  e.  q  /\  q  e.  A )  ->  Tr  q ) ) )
17 trel 4310 . . . . . . . . 9  |-  ( Tr  q  ->  ( (
z  e.  y  /\  y  e.  q )  ->  z  e.  q ) )
1817exp3acom3r 1380 . . . . . . . 8  |-  ( z  e.  y  ->  (
y  e.  q  -> 
( Tr  q  -> 
z  e.  q ) ) )
196, 8, 16, 18ee233 28603 . . . . . . 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 4021 . . . . . . . 8  |-  ( ( z  e.  q  /\  q  e.  A )  ->  z  e.  U. A
)
2120ex 425 . . . . . . 7  |-  ( z  e.  q  ->  (
q  e.  A  -> 
z  e.  U. A
) )
2219, 10, 21ee33 28606 . . . . . 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 1644 . . . . 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 1915 . . . . 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 219 . . . 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 39 . . 3  |-  ( A. x  e.  A  Tr  x  ->  ( ( z  e.  y  /\  y  e.  U. A )  -> 
z  e.  U. A
) )
2726alrimivv 1643 . 2  |-  ( A. x  e.  A  Tr  x  ->  A. z A. y
( ( z  e.  y  /\  y  e. 
U. A )  -> 
z  e.  U. A
) )
28 dftr2 4305 . 2  |-  ( Tr 
U. A  <->  A. z A. y ( ( z  e.  y  /\  y  e.  U. A )  -> 
z  e.  U. A
) )
2927, 28sylibr 205 1  |-  ( A. x  e.  A  Tr  x  ->  Tr  U. A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   A.wal 1550   E.wex 1551    e. wcel 1726   A.wral 2706   [.wsbc 3162   U.cuni 4016   Tr wtr 4303
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ral 2711  df-v 2959  df-sbc 3163  df-in 3328  df-ss 3335  df-uni 4017  df-tr 4304
  Copyright terms: Public domain W3C validator