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

Theorem truniALTVD 28990
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 28626 is truniALTVD 28990 without virtual deductions and was automatically derived from truniALTVD 28990.
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 28714 . . . . . . . 8  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  ( z  e.  y  /\  y  e.  U. A ) ).
2 simpr 448 . . . . . . . 8  |-  ( ( z  e.  y  /\  y  e.  U. A )  ->  y  e.  U. A )
31, 2e2 28732 . . . . . . 7  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  y  e.  U. A ).
4 eluni 4018 . . . . . . . 8  |-  ( y  e.  U. A  <->  E. q
( y  e.  q  /\  q  e.  A
) )
54biimpi 187 . . . . . . 7  |-  ( y  e.  U. A  ->  E. q ( y  e.  q  /\  q  e.  A ) )
63, 5e2 28732 . . . . . 6  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  E. q
( y  e.  q  /\  q  e.  A
) ).
7 simpl 444 . . . . . . . . . . . 12  |-  ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  y )
81, 7e2 28732 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  z  e.  y ).
9 idn3 28716 . . . . . . . . . . . 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 444 . . . . . . . . . . . 12  |-  ( ( y  e.  q  /\  q  e.  A )  ->  y  e.  q )
119, 10e3 28849 . . . . . . . . . . 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 448 . . . . . . . . . . . . 13  |-  ( ( y  e.  q  /\  q  e.  A )  ->  q  e.  A )
139, 12e3 28849 . . . . . . . . . . . 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 28665 . . . . . . . . . . . . 13  |-  (. A. x  e.  A  Tr  x 
->.  A. x  e.  A  Tr  x ).
15 rspsbc 3239 . . . . . . . . . . . . . 14  |-  ( q  e.  A  ->  ( A. x  e.  A  Tr  x  ->  [. q  /  x ]. Tr  x
) )
1615com12 29 . . . . . . . . . . . . 13  |-  ( A. x  e.  A  Tr  x  ->  ( q  e.  A  ->  [. q  /  x ]. Tr  x ) )
1714, 13, 16e13 28860 . . . . . . . . . . . 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 28625 . . . . . . . . . . . . 13  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  <->  Tr  q
) )
1918biimpd 199 . . . . . . . . . . . 12  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  ->  Tr  q ) )
2013, 17, 19e33 28846 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A ) ,. ( y  e.  q  /\  q  e.  A
) 
->.  Tr  q ).
21 trel 4309 . . . . . . . . . . . 12  |-  ( Tr  q  ->  ( (
z  e.  y  /\  y  e.  q )  ->  z  e.  q ) )
2221exp3acom3r 1379 . . . . . . . . . . 11  |-  ( z  e.  y  ->  (
y  e.  q  -> 
( Tr  q  -> 
z  e.  q ) ) )
238, 11, 20, 22e233 28877 . . . . . . . . . 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 4020 . . . . . . . . . . 11  |-  ( ( z  e.  q  /\  q  e.  A )  ->  z  e.  U. A
)
2524ex 424 . . . . . . . . . 10  |-  ( z  e.  q  ->  (
q  e.  A  -> 
z  e.  U. A
) )
2623, 13, 25e33 28846 . . . . . . . . 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 28710 . . . . . . . 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 28720 . . . . . . 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 1914 . . . . . . . 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 187 . . . . . . 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 28732 . . . . . 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 37 . . . . . 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 28772 . . . . 5  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  z  e.  U. A ).
3433in2 28706 . . . 4  |-  (. A. x  e.  A  Tr  x 
->.  ( ( z  e.  y  /\  y  e. 
U. A )  -> 
z  e.  U. A
) ).
3534gen12 28719 . . 3  |-  (. A. x  e.  A  Tr  x 
->.  A. z A. y
( ( z  e.  y  /\  y  e. 
U. A )  -> 
z  e.  U. A
) ).
36 dftr2 4304 . . . 4  |-  ( Tr 
U. A  <->  A. z A. y ( ( z  e.  y  /\  y  e.  U. A )  -> 
z  e.  U. A
) )
3736biimpri 198 . . 3  |-  ( A. z A. y ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  U. A )  ->  Tr  U. A )
3835, 37e1_ 28728 . 2  |-  (. A. x  e.  A  Tr  x 
->.  Tr  U. A ).
3938in1 28662 1  |-  ( A. x  e.  A  Tr  x  ->  Tr  U. A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1549   E.wex 1550    e. wcel 1725   A.wral 2705   [.wsbc 3161   U.cuni 4015   Tr wtr 4302
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2710  df-v 2958  df-sbc 3162  df-in 3327  df-ss 3334  df-uni 4016  df-tr 4303  df-vd1 28661  df-vd2 28670  df-vd3 28682
  Copyright terms: Public domain W3C validator