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 ⊢ A ∈ V → ⦋ A / x⦌ Pred R D X = Pred ⦋ A / x⦌ R ⦋ A / x⦌ D ⦋ A / x⦌ X

Proof

Step Hyp Ref Expression
1 csbin ⊢ ⦋ A / x⦌ D ∩ R -1 X = ⦋ A / x⦌ D ∩ ⦋ A / x⦌ R -1 X
2 csbima12 ⊢ ⦋ A / x⦌ R -1 X = ⦋ A / x⦌ R -1 ⦋ A / x⦌ X
3 csbcnv ⊢ ⦋ A / x⦌ R -1 = ⦋ A / x⦌ R -1
4 3 imaeq1i ⊢ ⦋ A / x⦌ R -1 ⦋ A / x⦌ X = ⦋ A / x⦌ R -1 ⦋ A / x⦌ X
5 csbsng ⊢ A ∈ V → ⦋ A / x⦌ X = ⦋ A / x⦌ X
6 5 imaeq2d ⊢ A ∈ V → ⦋ A / x⦌ R -1 ⦋ A / x⦌ X = ⦋ A / x⦌ R -1 ⦋ A / x⦌ X
7 4 6 eqtr3id ⊢ A ∈ V → ⦋ A / x⦌ R -1 ⦋ A / x⦌ X = ⦋ A / x⦌ R -1 ⦋ A / x⦌ X
8 2 7 eqtrid ⊢ A ∈ V → ⦋ A / x⦌ R -1 X = ⦋ A / x⦌ R -1 ⦋ A / x⦌ X
9 8 ineq2d ⊢ A ∈ V → ⦋ A / x⦌ D ∩ ⦋ A / x⦌ R -1 X = ⦋ A / x⦌ D ∩ ⦋ A / x⦌ R -1 ⦋ A / x⦌ X
10 1 9 eqtrid ⊢ A ∈ V → ⦋ A / x⦌ D ∩ R -1 X = ⦋ A / x⦌ D ∩ ⦋ A / x⦌ R -1 ⦋ A / x⦌ X
11 df-pred ⊢ Pred R D X = D ∩ R -1 X
12 11 csbeq2i ⊢ ⦋ A / x⦌ Pred R D X = ⦋ A / x⦌ D ∩ R -1 X
13 df-pred ⊢ Pred ⦋ A / x⦌ R ⦋ A / x⦌ D ⦋ A / x⦌ X = ⦋ A / x⦌ D ∩ ⦋ A / x⦌ R -1 ⦋ A / x⦌ X
14 10 12 13 3eqtr4g ⊢ A ∈ V → ⦋ A / x⦌ Pred R D X = Pred ⦋ A / x⦌ R ⦋ A / x⦌ D ⦋ A / x⦌ X