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

Metamath Proof Explorer

Theorem csbpredg

Description: Move class substitution in and out of the predecessor class of a relation. (Contributed by ML, 25-Oct-2020)

Ref Expression
Assertion csbpredg ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑋 ) = Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 csbin ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐷 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∩ ⦋ 𝐴 / 𝑥 ⦌ ( ◡ 𝑅 “ { 𝑋 } ) )
2 csbima12 ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( ◡ 𝑅 “ { 𝑋 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝑅 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝑋 } )
3 csbcnv ⊢ ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 = ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝑅
4 3 imaeq1i ⊢ ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝑋 } ) = ( ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝑅 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝑋 } )
5 csbsng ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ { 𝑋 } = { ⦋ 𝐴 / 𝑥 ⦌ 𝑋 } )
6 5 imaeq2d ⊢ ( 𝐴 ∈ 𝑉 → ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝑋 } ) = ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝑋 } ) )
7 4 6 eqtr3id ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ ◡ 𝑅 “ ⦋ 𝐴 / 𝑥 ⦌ { 𝑋 } ) = ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝑋 } ) )
8 2 7 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( ◡ 𝑅 “ { 𝑋 } ) = ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝑋 } ) )
9 8 ineq2d ⊢ ( 𝐴 ∈ 𝑉 → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∩ ⦋ 𝐴 / 𝑥 ⦌ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∩ ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝑋 } ) ) )
10 1 9 eqtrid ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐷 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∩ ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝑋 } ) ) )
11 df-pred ⊢ Pred ( 𝑅 , 𝐷 , 𝑋 ) = ( 𝐷 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
12 11 csbeq2i ⊢ ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑋 ) = ⦋ 𝐴 / 𝑥 ⦌ ( 𝐷 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
13 df-pred ⊢ Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝑋 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐷 ∩ ( ◡ ⦋ 𝐴 / 𝑥 ⦌ 𝑅 “ { ⦋ 𝐴 / 𝑥 ⦌ 𝑋 } ) )
14 10 12 13 3eqtr4g ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ Pred ( 𝑅 , 𝐷 , 𝑋 ) = Pred ( ⦋ 𝐴 / 𝑥 ⦌ 𝑅 , ⦋ 𝐴 / 𝑥 ⦌ 𝐷 , ⦋ 𝐴 / 𝑥 ⦌ 𝑋 ) )