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

Theorem truniALTVD 33411
Description: The union of a class of transitive sets is transitive. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. truniALT 33045 is truniALTVD 33411 without virtual deductions and was automatically derived from truniALTVD 33411.
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.  U. A )  ->.  ( z  e.  y  /\  y  e.  U. A ) ).
3:2:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  z  e.  y ).
4:2:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  y  e.  U. A ).
5:4:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  E. q ( y  e.  q  /\  q  e.  A ) ).
6::  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  ( y  e.  q  /\  q  e.  A ) ).
7:6:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  y  e.  q ).
8:6:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  q  e.  A ).
9:1,8:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  [ q  /  x ] Tr  x ).
10:8,9:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  Tr  q ).
11:3,7,10:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  z  e.  q ).
12:11,8:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A ) ,  ( y  e.  q  /\  q  e.  A )  ->.  z  e.  U. A ).
13:12:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  ( ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A ) ).
14:13:  |-  (. 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 ) ).
15:14:  |-  (. 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 ) ).
16:5,15:  |-  (. A. x  e.  A Tr  x ,. ( z  e.  y  /\  y  e.  U. A )  ->.  z  e.  U. A ).
17:16:  |-  (. A. x  e.  A Tr  x  ->.  ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  U. A ) ).
18:17:  |-  (. A. x  e.  A Tr  x  ->.  A. z A. y ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  U. A ) ).
19:18:  |-  (. A. x  e.  A Tr  x  ->.  Tr  U. A ).
qed:19:  |-  ( A. x  e.  A Tr  x  ->  Tr  U. A )
(Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
truniALTVD  |-  ( A. x  e.  A  Tr  x  ->  Tr  U. A )
Distinct variable group:    x, A

Proof of Theorem truniALTVD
Dummy variables  q 
y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn2 33132 . . . . . . . 8  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  ( z  e.  y  /\  y  e.  U. A ) ).
2 simpr 461 . . . . . . . 8  |-  ( ( z  e.  y  /\  y  e.  U. A )  ->  y  e.  U. A )
31, 2e2 33150 . . . . . . 7  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  y  e.  U. A ).
4 eluni 4237 . . . . . . . 8  |-  ( y  e.  U. A  <->  E. q
( y  e.  q  /\  q  e.  A
) )
54biimpi 194 . . . . . . 7  |-  ( y  e.  U. A  ->  E. q ( y  e.  q  /\  q  e.  A ) )
63, 5e2 33150 . . . . . 6  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  E. q
( y  e.  q  /\  q  e.  A
) ).
7 simpl 457 . . . . . . . . . . . 12  |-  ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  y )
81, 7e2 33150 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  z  e.  y ).
9 idn3 33134 . . . . . . . . . . . 12  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A ) ,. ( y  e.  q  /\  q  e.  A
) 
->.  ( y  e.  q  /\  q  e.  A
) ).
10 simpl 457 . . . . . . . . . . . 12  |-  ( ( y  e.  q  /\  q  e.  A )  ->  y  e.  q )
119, 10e3 33267 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A ) ,. ( y  e.  q  /\  q  e.  A
) 
->.  y  e.  q ).
12 simpr 461 . . . . . . . . . . . . 13  |-  ( ( y  e.  q  /\  q  e.  A )  ->  q  e.  A )
139, 12e3 33267 . . . . . . . . . . . 12  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A ) ,. ( y  e.  q  /\  q  e.  A
) 
->.  q  e.  A ).
14 idn1 33084 . . . . . . . . . . . . 13  |-  (. A. x  e.  A  Tr  x 
->.  A. x  e.  A  Tr  x ).
15 rspsbc 3403 . . . . . . . . . . . . . 14  |-  ( q  e.  A  ->  ( A. x  e.  A  Tr  x  ->  [. q  /  x ]. Tr  x
) )
1615com12 31 . . . . . . . . . . . . 13  |-  ( A. x  e.  A  Tr  x  ->  ( q  e.  A  ->  [. q  /  x ]. Tr  x ) )
1714, 13, 16e13 33278 . . . . . . . . . . . 12  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A ) ,. ( y  e.  q  /\  q  e.  A
) 
->.  [. q  /  x ]. Tr  x ).
18 trsbc 33044 . . . . . . . . . . . . 13  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  <->  Tr  q
) )
1918biimpd 207 . . . . . . . . . . . 12  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  ->  Tr  q ) )
2013, 17, 19e33 33264 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A ) ,. ( y  e.  q  /\  q  e.  A
) 
->.  Tr  q ).
21 trel 4537 . . . . . . . . . . . 12  |-  ( Tr  q  ->  ( (
z  e.  y  /\  y  e.  q )  ->  z  e.  q ) )
2221expdcom 439 . . . . . . . . . . 11  |-  ( z  e.  y  ->  (
y  e.  q  -> 
( Tr  q  -> 
z  e.  q ) ) )
238, 11, 20, 22e233 33295 . . . . . . . . . 10  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A ) ,. ( y  e.  q  /\  q  e.  A
) 
->.  z  e.  q ).
24 elunii 4239 . . . . . . . . . . 11  |-  ( ( z  e.  q  /\  q  e.  A )  ->  z  e.  U. A
)
2524ex 434 . . . . . . . . . 10  |-  ( z  e.  q  ->  (
q  e.  A  -> 
z  e.  U. A
) )
2623, 13, 25e33 33264 . . . . . . . . 9  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A ) ,. ( y  e.  q  /\  q  e.  A
) 
->.  z  e.  U. A ).
2726in3 33128 . . . . . . . 8  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  ( (
y  e.  q  /\  q  e.  A )  ->  z  e.  U. A
) ).
2827gen21 33138 . . . . . . 7  |-  (. 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 ) ).
29 19.23v 1747 . . . . . . . 8  |-  ( A. q ( ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A )  <->  ( E. q ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A ) )
3029biimpi 194 . . . . . . 7  |-  ( A. q ( ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A )  -> 
( E. q ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A
) )
3128, 30e2 33150 . . . . . 6  |-  (. 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 ) ).
32 pm2.27 39 . . . . . 6  |-  ( E. q ( y  e.  q  /\  q  e.  A )  ->  (
( E. q ( y  e.  q  /\  q  e.  A )  ->  z  e.  U. A
)  ->  z  e.  U. A ) )
336, 31, 32e22 33190 . . . . 5  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  z  e.  U. A ).
3433in2 33124 . . . 4  |-  (. A. x  e.  A  Tr  x 
->.  ( ( z  e.  y  /\  y  e. 
U. A )  -> 
z  e.  U. A
) ).
3534gen12 33137 . . 3  |-  (. A. x  e.  A  Tr  x 
->.  A. z A. y
( ( z  e.  y  /\  y  e. 
U. A )  -> 
z  e.  U. A
) ).
36 dftr2 4532 . . . 4  |-  ( Tr 
U. A  <->  A. z A. y ( ( z  e.  y  /\  y  e.  U. A )  -> 
z  e.  U. A
) )
3736biimpri 206 . . 3  |-  ( A. z A. y ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  U. A )  ->  Tr  U. A )
3835, 37e1a 33146 . 2  |-  (. A. x  e.  A  Tr  x 
->.  Tr  U. A ).
3938in1 33081 1  |-  ( A. x  e.  A  Tr  x  ->  Tr  U. A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1381   E.wex 1599    e. wcel 1804   A.wral 2793   [.wsbc 3313   U.cuni 4234   Tr wtr 4530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-v 3097  df-sbc 3314  df-in 3468  df-ss 3475  df-uni 4235  df-tr 4531  df-vd1 33080  df-vd2 33088  df-vd3 33100
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator