This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ 𝑉 → ( TC ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑦 = 𝐴 → ( TC ‘ 𝑦 ) = ( TC ‘ 𝐴 ) )
2 sseq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥 ) )
3 2 anbi1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) ↔ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) ) )
4 3 abbidv ⊢ ( 𝑦 = 𝐴 → { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) } = { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
5 4 inteqd ⊢ ( 𝑦 = 𝐴 → ∩ { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) } = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
6 1 5 eqeq12d ⊢ ( 𝑦 = 𝐴 → ( ( TC ‘ 𝑦 ) = ∩ { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) } ↔ ( TC ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } ) )
7 vex ⊢ 𝑦 ∈ V
8 7 tz9.1c ⊢ ∩ { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V
9 df-tc ⊢ TC = ( 𝑦 ∈ V ↦ ∩ { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
10 9 fvmpt2 ⊢ ( ( 𝑦 ∈ V ∧ ∩ { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) } ∈ V ) → ( TC ‘ 𝑦 ) = ∩ { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) } )
11 7 8 10 mp2an ⊢ ( TC ‘ 𝑦 ) = ∩ { 𝑥 ∣ ( 𝑦 ⊆ 𝑥 ∧ Tr 𝑥 ) }
12 6 11 vtoclg ⊢ ( 𝐴 ∈ 𝑉 → ( TC ‘ 𝐴 ) = ∩ { 𝑥 ∣ ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) } )