Metamath Proof Explorer


Theorem tcvalg

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 AVTCA=x|AxTrx

Proof

Step Hyp Ref Expression
1 fveq2 y=ATCy=TCA
2 sseq1 y=AyxAx
3 2 anbi1d y=AyxTrxAxTrx
4 3 abbidv y=Ax|yxTrx=x|AxTrx
5 4 inteqd y=Ax|yxTrx=x|AxTrx
6 1 5 eqeq12d y=ATCy=x|yxTrxTCA=x|AxTrx
7 vex yV
8 7 tz9.1c x|yxTrxV
9 df-tc TC=yVx|yxTrx
10 9 fvmpt2 yVx|yxTrxVTCy=x|yxTrx
11 7 8 10 mp2an TCy=x|yxTrx
12 6 11 vtoclg AVTCA=x|AxTrx