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

Theorem truniALTVD 37275
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 36902 is truniALTVD 37275 without virtual deductions and was automatically derived from truniALTVD 37275.
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 36992 . . . . . . . 8  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  ( z  e.  y  /\  y  e.  U. A ) ).
2 simpr 463 . . . . . . . 8  |-  ( ( z  e.  y  /\  y  e.  U. A )  ->  y  e.  U. A )
31, 2e2 37010 . . . . . . 7  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  y  e.  U. A ).
4 eluni 4201 . . . . . . . 8  |-  ( y  e.  U. A  <->  E. q
( y  e.  q  /\  q  e.  A
) )
54biimpi 198 . . . . . . 7  |-  ( y  e.  U. A  ->  E. q ( y  e.  q  /\  q  e.  A ) )
63, 5e2 37010 . . . . . 6  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  E. q
( y  e.  q  /\  q  e.  A
) ).
7 simpl 459 . . . . . . . . . . . 12  |-  ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  y )
81, 7e2 37010 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  z  e.  y ).
9 idn3 36994 . . . . . . . . . . . 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 459 . . . . . . . . . . . 12  |-  ( ( y  e.  q  /\  q  e.  A )  ->  y  e.  q )
119, 10e3 37124 . . . . . . . . . . 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 463 . . . . . . . . . . . . 13  |-  ( ( y  e.  q  /\  q  e.  A )  ->  q  e.  A )
139, 12e3 37124 . . . . . . . . . . . 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 36944 . . . . . . . . . . . . 13  |-  (. A. x  e.  A  Tr  x 
->.  A. x  e.  A  Tr  x ).
15 rspsbc 3346 . . . . . . . . . . . . . 14  |-  ( q  e.  A  ->  ( A. x  e.  A  Tr  x  ->  [. q  /  x ]. Tr  x
) )
1615com12 32 . . . . . . . . . . . . 13  |-  ( A. x  e.  A  Tr  x  ->  ( q  e.  A  ->  [. q  /  x ]. Tr  x ) )
1714, 13, 16e13 37135 . . . . . . . . . . . 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 36901 . . . . . . . . . . . . 13  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  <->  Tr  q
) )
1918biimpd 211 . . . . . . . . . . . 12  |-  ( q  e.  A  ->  ( [. q  /  x ]. Tr  x  ->  Tr  q ) )
2013, 17, 19e33 37121 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A ) ,. ( y  e.  q  /\  q  e.  A
) 
->.  Tr  q ).
21 trel 4504 . . . . . . . . . . . 12  |-  ( Tr  q  ->  ( (
z  e.  y  /\  y  e.  q )  ->  z  e.  q ) )
2221expdcom 441 . . . . . . . . . . 11  |-  ( z  e.  y  ->  (
y  e.  q  -> 
( Tr  q  -> 
z  e.  q ) ) )
238, 11, 20, 22e233 37152 . . . . . . . . . 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 4203 . . . . . . . . . . 11  |-  ( ( z  e.  q  /\  q  e.  A )  ->  z  e.  U. A
)
2524ex 436 . . . . . . . . . 10  |-  ( z  e.  q  ->  (
q  e.  A  -> 
z  e.  U. A
) )
2623, 13, 25e33 37121 . . . . . . . . 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 36988 . . . . . . . 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 36998 . . . . . . 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 1818 . . . . . . . 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 198 . . . . . . 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 37010 . . . . . 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 40 . . . . . 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 37050 . . . . 5  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  z  e.  U. A ).
3433in2 36984 . . . 4  |-  (. A. x  e.  A  Tr  x 
->.  ( ( z  e.  y  /\  y  e. 
U. A )  -> 
z  e.  U. A
) ).
3534gen12 36997 . . 3  |-  (. A. x  e.  A  Tr  x 
->.  A. z A. y
( ( z  e.  y  /\  y  e. 
U. A )  -> 
z  e.  U. A
) ).
36 dftr2 4499 . . . 4  |-  ( Tr 
U. A  <->  A. z A. y ( ( z  e.  y  /\  y  e.  U. A )  -> 
z  e.  U. A
) )
3736biimpri 210 . . 3  |-  ( A. z A. y ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  U. A )  ->  Tr  U. A )
3835, 37e1a 37006 . 2  |-  (. A. x  e.  A  Tr  x 
->.  Tr  U. A ).
3938in1 36941 1  |-  ( A. x  e.  A  Tr  x  ->  Tr  U. A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371   A.wal 1442   E.wex 1663    e. wcel 1887   A.wral 2737   [.wsbc 3267   U.cuni 4198   Tr wtr 4497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2742  df-v 3047  df-sbc 3268  df-in 3411  df-ss 3418  df-uni 4199  df-tr 4498  df-vd1 36940  df-vd2 36948  df-vd3 36960
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator