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

Theorem truniALTVD 28970
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 O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. truniALT 28604 is truniALTVD 28970 without virtual deductions and was automatically derived from truniALTVD 28970.
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 28690 . . . . . . . 8  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  ( z  e.  y  /\  y  e.  U. A ) ).
2 simpr 447 . . . . . . . 8  |-  ( ( z  e.  y  /\  y  e.  U. A )  ->  y  e.  U. A )
31, 2e2 28708 . . . . . . 7  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  y  e.  U. A ).
4 eluni 3846 . . . . . . . 8  |-  ( y  e.  U. A  <->  E. q
( y  e.  q  /\  q  e.  A
) )
54biimpi 186 . . . . . . 7  |-  ( y  e.  U. A  ->  E. q ( y  e.  q  /\  q  e.  A ) )
63, 5e2 28708 . . . . . 6  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  E. q
( y  e.  q  /\  q  e.  A
) ).
7 simpl 443 . . . . . . . . . . . 12  |-  ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  y )
81, 7e2 28708 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  z  e.  y ).
9 idn3 28692 . . . . . . . . . . . 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 443 . . . . . . . . . . . 12  |-  ( ( y  e.  q  /\  q  e.  A )  ->  y  e.  q )
119, 10e3 28826 . . . . . . . . . . 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 447 . . . . . . . . . . . . 13  |-  ( ( y  e.  q  /\  q  e.  A )  ->  q  e.  A )
139, 12e3 28826 . . . . . . . . . . . 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 28641 . . . . . . . . . . . . 13  |-  (. A. x  e.  A  Tr  x 
->.  A. x  e.  A  Tr  x ).
15 rspsbc 3082 . . . . . . . . . . . . . 14  |-  ( q  e.  A  ->  ( A. x  e.  A  Tr  x  ->  [. q  /  x ]. Tr  x
) )
1615com12 27 . . . . . . . . . . . . 13  |-  ( A. x  e.  A  Tr  x  ->  ( q  e.  A  ->  [. q  /  x ]. Tr  x ) )
1714, 13, 16e13 28837 . . . . . . . . . . . 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 28603 . . . . . . . . . . . . 13  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  <->  Tr  q
) )
1918biimpd 198 . . . . . . . . . . . 12  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  ->  Tr  q ) )
2013, 17, 19e33 28823 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A ) ,. ( y  e.  q  /\  q  e.  A
) 
->.  Tr  q ).
21 trel 4136 . . . . . . . . . . . 12  |-  ( Tr  q  ->  ( (
z  e.  y  /\  y  e.  q )  ->  z  e.  q ) )
2221exp3acom3r 1360 . . . . . . . . . . 11  |-  ( z  e.  y  ->  (
y  e.  q  -> 
( Tr  q  -> 
z  e.  q ) ) )
238, 11, 20, 22e233 28854 . . . . . . . . . 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 3848 . . . . . . . . . . 11  |-  ( ( z  e.  q  /\  q  e.  A )  ->  z  e.  U. A
)
2524ex 423 . . . . . . . . . 10  |-  ( z  e.  q  ->  (
q  e.  A  -> 
z  e.  U. A
) )
2623, 13, 25e33 28823 . . . . . . . . 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 28686 . . . . . . . 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 28696 . . . . . . 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 1844 . . . . . . . 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 186 . . . . . . 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 28708 . . . . . 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 35 . . . . . 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 28748 . . . . 5  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  z  e.  U. A ).
3433in2 28682 . . . 4  |-  (. A. x  e.  A  Tr  x 
->.  ( ( z  e.  y  /\  y  e. 
U. A )  -> 
z  e.  U. A
) ).
3534gen12 28695 . . 3  |-  (. A. x  e.  A  Tr  x 
->.  A. z A. y
( ( z  e.  y  /\  y  e. 
U. A )  -> 
z  e.  U. A
) ).
36 dftr2 4131 . . . 4  |-  ( Tr 
U. A  <->  A. z A. y ( ( z  e.  y  /\  y  e.  U. A )  -> 
z  e.  U. A
) )
3736biimpri 197 . . 3  |-  ( A. z A. y ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  U. A )  ->  Tr  U. A )
3835, 37e1_ 28704 . 2  |-  (. A. x  e.  A  Tr  x 
->.  Tr  U. A ).
3938in1 28638 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  df-vd1 28637  df-vd2 28646  df-vd3 28658
  Copyright terms: Public domain W3C validator