Description: Value of the transitive closure function. (The fact that this intersection exists is a non-trivial fact that depends on ax-inf ; see tz9.1 .) (Contributed by Mario Carneiro, 23-Jun-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | tcvalg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 | |
|
2 | sseq1 | |
|
3 | 2 | anbi1d | |
4 | 3 | abbidv | |
5 | 4 | inteqd | |
6 | 1 5 | eqeq12d | |
7 | vex | |
|
8 | 7 | tz9.1c | |
9 | df-tc | |
|
10 | 9 | fvmpt2 | |
11 | 7 8 10 | mp2an | |
12 | 6 11 | vtoclg | |