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 xATrBTrxAB

Proof

Step Hyp Ref Expression
1 eliun yxABxAyB
2 r19.29 xATrBxAyBxATrByB
3 nfcv _xy
4 nfiu1 _xxAB
5 3 4 nfss xyxAB
6 trss TrByByB
7 6 imp TrByByB
8 ssiun2 xABxAB
9 sstr2 yBBxAByxAB
10 7 8 9 syl2imc xATrByByxAB
11 5 10 rexlimi xATrByByxAB
12 2 11 syl xATrBxAyByxAB
13 1 12 sylan2b xATrByxAByxAB
14 13 ralrimiva xATrByxAByxAB
15 dftr3 TrxAByxAByxAB
16 14 15 sylibr xATrBTrxAB