Description: An indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | triun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eliun | |
|
2 | r19.29 | |
|
3 | nfcv | |
|
4 | nfiu1 | |
|
5 | 3 4 | nfss | |
6 | trss | |
|
7 | 6 | imp | |
8 | ssiun2 | |
|
9 | sstr2 | |
|
10 | 7 8 9 | syl2imc | |
11 | 5 10 | rexlimi | |
12 | 2 11 | syl | |
13 | 1 12 | sylan2b | |
14 | 13 | ralrimiva | |
15 | dftr3 | |
|
16 | 14 15 | sylibr | |