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

Theorem truniALTVD 34098
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 33721 is truniALTVD 34098 without virtual deductions and was automatically derived from truniALTVD 34098.
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 33812 . . . . . . . 8  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  ( z  e.  y  /\  y  e.  U. A ) ).
2 simpr 459 . . . . . . . 8  |-  ( ( z  e.  y  /\  y  e.  U. A )  ->  y  e.  U. A )
31, 2e2 33830 . . . . . . 7  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  y  e.  U. A ).
4 eluni 4238 . . . . . . . 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 33830 . . . . . 6  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  E. q
( y  e.  q  /\  q  e.  A
) ).
7 simpl 455 . . . . . . . . . . . 12  |-  ( ( z  e.  y  /\  y  e.  U. A )  ->  z  e.  y )
81, 7e2 33830 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  z  e.  y ).
9 idn3 33814 . . . . . . . . . . . 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 455 . . . . . . . . . . . 12  |-  ( ( y  e.  q  /\  q  e.  A )  ->  y  e.  q )
119, 10e3 33947 . . . . . . . . . . 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 459 . . . . . . . . . . . . 13  |-  ( ( y  e.  q  /\  q  e.  A )  ->  q  e.  A )
139, 12e3 33947 . . . . . . . . . . . 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 33764 . . . . . . . . . . . . 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 33958 . . . . . . . . . . . 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 33720 . . . . . . . . . . . . 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 33944 . . . . . . . . . . 11  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A ) ,. ( y  e.  q  /\  q  e.  A
) 
->.  Tr  q ).
21 trel 4539 . . . . . . . . . . . 12  |-  ( Tr  q  ->  ( (
z  e.  y  /\  y  e.  q )  ->  z  e.  q ) )
2221expdcom 437 . . . . . . . . . . 11  |-  ( z  e.  y  ->  (
y  e.  q  -> 
( Tr  q  -> 
z  e.  q ) ) )
238, 11, 20, 22e233 33975 . . . . . . . . . 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 4240 . . . . . . . . . . 11  |-  ( ( z  e.  q  /\  q  e.  A )  ->  z  e.  U. A
)
2524ex 432 . . . . . . . . . 10  |-  ( z  e.  q  ->  (
q  e.  A  -> 
z  e.  U. A
) )
2623, 13, 25e33 33944 . . . . . . . . 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 33808 . . . . . . . 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 33818 . . . . . . 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 1765 . . . . . . . 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 33830 . . . . . 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 33870 . . . . 5  |-  (. A. x  e.  A  Tr  x ,. ( z  e.  y  /\  y  e. 
U. A )  ->.  z  e.  U. A ).
3433in2 33804 . . . 4  |-  (. A. x  e.  A  Tr  x 
->.  ( ( z  e.  y  /\  y  e. 
U. A )  -> 
z  e.  U. A
) ).
3534gen12 33817 . . 3  |-  (. A. x  e.  A  Tr  x 
->.  A. z A. y
( ( z  e.  y  /\  y  e. 
U. A )  -> 
z  e.  U. A
) ).
36 dftr2 4534 . . . 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 33826 . 2  |-  (. A. x  e.  A  Tr  x 
->.  Tr  U. A ).
3938in1 33761 1  |-  ( A. x  e.  A  Tr  x  ->  Tr  U. A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367   A.wal 1396   E.wex 1617    e. wcel 1823   A.wral 2804   [.wsbc 3324   U.cuni 4235   Tr wtr 4532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-v 3108  df-sbc 3325  df-in 3468  df-ss 3475  df-uni 4236  df-tr 4533  df-vd1 33760  df-vd2 33768  df-vd3 33780
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator