This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem trintALT

Description: The intersection of a class of transitive sets is transitive. Exercise 5(b) of Enderton p. 73. trintALT is an alternate proof of trint . trintALT is trintALTVD without virtual deductions and was automatically derived from trintALTVD using the tools program translate..without..overwriting.cmd and the Metamath program "MM-PA> MINIMIZE__WITH *" command. (Contributed by Alan Sare, 17-Apr-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion trintALT 
|- ( A. x e. A Tr x -> Tr |^| A )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( z e. y /\ y e. |^| A ) -> z e. y )
2 1 a1i 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> z e. y ) )
3 iidn3 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> ( q e. A -> q e. A ) ) )
4 id 
 |-  ( A. x e. A Tr x -> A. x e. A Tr x )
5 rspsbc 
 |-  ( q e. A -> ( A. x e. A Tr x -> [. q / x ]. Tr x ) )
6 3 4 5 ee31 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> ( q e. A -> [. q / x ]. Tr x ) ) )
7 trsbc 
 |-  ( q e. A -> ( [. q / x ]. Tr x <-> Tr q ) )
8 7 biimpd 
 |-  ( q e. A -> ( [. q / x ]. Tr x -> Tr q ) )
9 3 6 8 ee33 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> ( q e. A -> Tr q ) ) )
10 simpr 
 |-  ( ( z e. y /\ y e. |^| A ) -> y e. |^| A )
11 10 a1i 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> y e. |^| A ) )
12 elintg 
 |-  ( y e. |^| A -> ( y e. |^| A <-> A. q e. A y e. q ) )
13 12 ibi 
 |-  ( y e. |^| A -> A. q e. A y e. q )
14 11 13 syl6 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> A. q e. A y e. q ) )
15 rsp 
 |-  ( A. q e. A y e. q -> ( q e. A -> y e. q ) )
16 14 15 syl6 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> ( q e. A -> y e. q ) ) )
17 trel 
 |-  ( Tr q -> ( ( z e. y /\ y e. q ) -> z e. q ) )
18 17 expd 
 |-  ( Tr q -> ( z e. y -> ( y e. q -> z e. q ) ) )
19 9 2 16 18 ee323 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> ( q e. A -> z e. q ) ) )
20 19 ralrimdv 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> A. q e. A z e. q ) )
21 elintg 
 |-  ( z e. y -> ( z e. |^| A <-> A. q e. A z e. q ) )
22 21 biimprd 
 |-  ( z e. y -> ( A. q e. A z e. q -> z e. |^| A ) )
23 2 20 22 syl6c 
 |-  ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> z e. |^| A ) )
24 23 alrimivv 
 |-  ( A. x e. A Tr x -> A. z A. y ( ( z e. y /\ y e. |^| A ) -> z e. |^| A ) )
25 dftr2 
 |-  ( Tr |^| A <-> A. z A. y ( ( z e. y /\ y e. |^| A ) -> z e. |^| A ) )
26 24 25 sylibr 
 |-  ( A. x e. A Tr x -> Tr |^| A )