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

Metamath Proof Explorer

Theorem triun

Description: An indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion triun 
|- ( A. x e. A Tr B -> Tr U_ x e. A B )

Proof

Step Hyp Ref Expression
1 eliun 
 |-  ( y e. U_ x e. A B <-> E. x e. A y e. B )
2 r19.29 
 |-  ( ( A. x e. A Tr B /\ E. x e. A y e. B ) -> E. x e. A ( Tr B /\ y e. B ) )
3 nfcv 
 |-  F/_ x y
4 nfiu1 
 |-  F/_ x U_ x e. A B
5 3 4 nfss 
 |-  F/ x y C_ U_ x e. A B
6 trss 
 |-  ( Tr B -> ( y e. B -> y C_ B ) )
7 6 imp 
 |-  ( ( Tr B /\ y e. B ) -> y C_ B )
8 ssiun2 
 |-  ( x e. A -> B C_ U_ x e. A B )
9 sstr2 
 |-  ( y C_ B -> ( B C_ U_ x e. A B -> y C_ U_ x e. A B ) )
10 7 8 9 syl2imc 
 |-  ( x e. A -> ( ( Tr B /\ y e. B ) -> y C_ U_ x e. A B ) )
11 5 10 rexlimi 
 |-  ( E. x e. A ( Tr B /\ y e. B ) -> y C_ U_ x e. A B )
12 2 11 syl 
 |-  ( ( A. x e. A Tr B /\ E. x e. A y e. B ) -> y C_ U_ x e. A B )
13 1 12 sylan2b 
 |-  ( ( A. x e. A Tr B /\ y e. U_ x e. A B ) -> y C_ U_ x e. A B )
14 13 ralrimiva 
 |-  ( A. x e. A Tr B -> A. y e. U_ x e. A B y C_ U_ x e. A B )
15 dftr3 
 |-  ( Tr U_ x e. A B <-> A. y e. U_ x e. A B y C_ U_ x e. A B )
16 14 15 sylibr 
 |-  ( A. x e. A Tr B -> Tr U_ x e. A B )