Metamath Proof Explorer

Theorem truniALT

Description: The union of a class of transitive sets is transitive. Alternate proof of truni . truniALT is truniALTVD without virtual deductions and was automatically derived from truniALTVD using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( z e. y /\ y e. U. A ) -> y e. U. A )
2 1 a1i 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> y e. U. A ) )
3 eluni 
 |-  ( y e. U. A <-> E. q ( y e. q /\ q e. A ) )
4 2 3 imbitrdi 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> E. q ( y e. q /\ q e. A ) ) )
5 simpl 
 |-  ( ( z e. y /\ y e. U. A ) -> z e. y )
6 5 a1i 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> z e. y ) )
7 simpl 
 |-  ( ( y e. q /\ q e. A ) -> y e. q )
8 7 2a1i 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> y e. q ) ) )
9 simpr 
 |-  ( ( y e. q /\ q e. A ) -> q e. A )
10 9 2a1i 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> q e. A ) ) )
11 rspsbc 
 |-  ( q e. A -> ( A. x e. A Tr x -> [. q / x ]. Tr x ) )
12 11 com12 
 |-  ( A. x e. A Tr x -> ( q e. A -> [. q / x ]. Tr x ) )
13 10 12 syl6d 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> [. q / x ]. Tr x ) ) )
14 trsbc 
 |-  ( q e. A -> ( [. q / x ]. Tr x <-> Tr q ) )
15 14 biimpd 
 |-  ( q e. A -> ( [. q / x ]. Tr x -> Tr q ) )
16 10 13 15 ee33 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> Tr q ) ) )
17 trel 
 |-  ( Tr q -> ( ( z e. y /\ y e. q ) -> z e. q ) )
18 17 expdcom 
 |-  ( z e. y -> ( y e. q -> ( Tr q -> z e. q ) ) )
19 6 8 16 18 ee233 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> z e. q ) ) )
20 elunii 
 |-  ( ( z e. q /\ q e. A ) -> z e. U. A )
21 20 ex 
 |-  ( z e. q -> ( q e. A -> z e. U. A ) )
22 19 10 21 ee33 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> z e. U. A ) ) )
23 22 alrimdv 
 |-  ( 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 ) ) )
24 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 ) )
25 23 24 imbitrdi 
 |-  ( 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 ) ) )
26 4 25 mpdd 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> z e. U. A ) )
27 26 alrimivv 
 |-  ( A. x e. A Tr x -> A. z A. y ( ( z e. y /\ y e. U. A ) -> z e. U. A ) )
28 dftr2 
 |-  ( Tr U. A <-> A. z A. y ( ( z e. y /\ y e. U. A ) -> z e. U. A ) )
29 27 28 sylibr 
 |-  ( A. x e. A Tr x -> Tr U. A )