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

Metamath Proof Explorer

Theorem triin

Description: An indexed intersection of a class of transitive sets is transitive. (Contributed by BJ, 3-Oct-2022)

Ref Expression
Assertion triin 
|- ( A. x e. A Tr B -> Tr |^|_ x e. A B )

Proof

Step Hyp Ref Expression
1 eliin 
 |-  ( y e. _V -> ( y e. |^|_ x e. A B <-> A. x e. A y e. B ) )
2 1 elv 
 |-  ( y e. |^|_ x e. A B <-> A. x e. A y e. B )
3 r19.26 
 |-  ( A. x e. A ( Tr B /\ y e. B ) <-> ( A. x e. A Tr B /\ A. x e. A y e. B ) )
4 trss 
 |-  ( Tr B -> ( y e. B -> y C_ B ) )
5 4 imp 
 |-  ( ( Tr B /\ y e. B ) -> y C_ B )
6 5 ralimi 
 |-  ( A. x e. A ( Tr B /\ y e. B ) -> A. x e. A y C_ B )
7 3 6 sylbir 
 |-  ( ( A. x e. A Tr B /\ A. x e. A y e. B ) -> A. x e. A y C_ B )
8 ssiin 
 |-  ( y C_ |^|_ x e. A B <-> A. x e. A y C_ B )
9 7 8 sylibr 
 |-  ( ( A. x e. A Tr B /\ A. x e. A y e. B ) -> y C_ |^|_ x e. A B )
10 2 9 sylan2b 
 |-  ( ( A. x e. A Tr B /\ y e. |^|_ x e. A B ) -> y C_ |^|_ x e. A B )
11 10 ralrimiva 
 |-  ( A. x e. A Tr B -> A. y e. |^|_ x e. A B y C_ |^|_ x e. A B )
12 dftr3 
 |-  ( Tr |^|_ x e. A B <-> A. y e. |^|_ x e. A B y C_ |^|_ x e. A B )
13 11 12 sylibr 
 |-  ( A. x e. A Tr B -> Tr |^|_ x e. A B )