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 )