Metamath Proof Explorer

Theorem truniALTVD

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 is truniALTVD without virtual deductions and was automatically derived from truniALTVD .

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.)

Ref Expression
Assertion truniALTVD 
|- ( A. x e. A Tr x -> Tr U. A )

Proof

Step Hyp Ref Expression
1 idn2 
 |-  (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. ( z e. y /\ y e. U. A ) ).
2 simpr 
 |-  ( ( z e. y /\ y e. U. A ) -> y e. U. A )
3 1 2 e2 
 |-  (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. y e. U. A ).
4 eluni 
 |-  ( y e. U. A <-> E. q ( y e. q /\ q e. A ) )
5 4 biimpi 
 |-  ( y e. U. A -> E. q ( y e. q /\ q e. A ) )
6 3 5 e2 
 |-  (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. E. q ( y e. q /\ q e. A ) ).
7 simpl 
 |-  ( ( z e. y /\ y e. U. A ) -> z e. y )
8 1 7 e2 
 |-  (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. z e. y ).
9 idn3 
 |-  (. 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 
 |-  ( ( y e. q /\ q e. A ) -> y e. q )
11 9 10 e3 
 |-  (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ,. ( y e. q /\ q e. A ) ->. y e. q ).
12 simpr 
 |-  ( ( y e. q /\ q e. A ) -> q e. A )
13 9 12 e3 
 |-  (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ,. ( y e. q /\ q e. A ) ->. q e. A ).
14 idn1 
 |-  (. A. x e. A Tr x ->. A. x e. A Tr x ).
15 rspsbc 
 |-  ( q e. A -> ( A. x e. A Tr x -> [. q / x ]. Tr x ) )
16 15 com12 
 |-  ( A. x e. A Tr x -> ( q e. A -> [. q / x ]. Tr x ) )
17 14 13 16 e13 
 |-  (. 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 
 |-  ( q e. A -> ( [. q / x ]. Tr x <-> Tr q ) )
19 18 biimpd 
 |-  ( q e. A -> ( [. q / x ]. Tr x -> Tr q ) )
20 13 17 19 e33 
 |-  (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ,. ( y e. q /\ q e. A ) ->. Tr q ).
21 trel 
 |-  ( Tr q -> ( ( z e. y /\ y e. q ) -> z e. q ) )
22 21 expdcom 
 |-  ( z e. y -> ( y e. q -> ( Tr q -> z e. q ) ) )
23 8 11 20 22 e233 
 |-  (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ,. ( y e. q /\ q e. A ) ->. z e. q ).
24 elunii 
 |-  ( ( z e. q /\ q e. A ) -> z e. U. A )
25 24 ex 
 |-  ( z e. q -> ( q e. A -> z e. U. A ) )
26 23 13 25 e33 
 |-  (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ,. ( y e. q /\ q e. A ) ->. z e. U. A ).
27 26 in3 
 |-  (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. ( ( y e. q /\ q e. A ) -> z e. U. A ) ).
28 27 gen21 
 |-  (. 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 
 |-  ( A. q ( ( y e. q /\ q e. A ) -> z e. U. A ) <-> ( E. q ( y e. q /\ q e. A ) -> z e. U. A ) )
30 29 biimpi 
 |-  ( A. q ( ( y e. q /\ q e. A ) -> z e. U. A ) -> ( E. q ( y e. q /\ q e. A ) -> z e. U. A ) )
31 28 30 e2 
 |-  (. 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 
 |-  ( E. q ( y e. q /\ q e. A ) -> ( ( E. q ( y e. q /\ q e. A ) -> z e. U. A ) -> z e. U. A ) )
33 6 31 32 e22 
 |-  (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. z e. U. A ).
34 33 in2 
 |-  (. A. x e. A Tr x ->. ( ( z e. y /\ y e. U. A ) -> z e. U. A ) ).
35 34 gen12 
 |-  (. A. x e. A Tr x ->. A. z A. y ( ( z e. y /\ y e. U. A ) -> z e. U. A ) ).
36 dftr2 
 |-  ( Tr U. A <-> A. z A. y ( ( z e. y /\ y e. U. A ) -> z e. U. A ) )
37 36 biimpri 
 |-  ( A. z A. y ( ( z e. y /\ y e. U. A ) -> z e. U. A ) -> Tr U. A )
38 35 37 e1a 
 |-  (. A. x e. A Tr x ->. Tr U. A ).
39 38 in1 
 |-  ( A. x e. A Tr x -> Tr U. A )