Metamath Proof Explorer

Theorem csbresgVD

Description: Virtual deduction proof of csbres . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. csbres is csbresgVD without virtual deductions and was automatically derived from csbresgVD .

1:: |- (. A e. V ->. A e. V ).
2:1: |- (. A e. V ->. [_ A / x ]_ V = V ).
3:2: |- (. A e. V ->. ( [_ A / x ]_ C X. [_ A / x ]_ V ) = ( [ A / x ]_ C X.V ) ).
4:1: |- (. A e. V ->. [ A / x ]_ ( C X.V ) = ( [ A / x ]_ C X. [_ A / x ]_ V ) ).
5:3,4: |- (. A e. V ->. [ A / x ]_ ( C X.V ) = ( [ A / x ]_ C X.V ) ).
6:5: |- (. A e. V ->. ( [ A / x ]_ B i^i [_ A / x ]_ ( C X.V ) ) = ( [ A / x ]_ B i^i ( [_ A / x ]_ C X.V ) ) ).
7:1: |- (. A e. V ->. [ A / x ]_ ( B i^i ( C X. _V ) ) = ( [_ A / x ]_ B i^i [_ A / x ]_ ( C X.V ) ) ).
8:6,7: |- (. A e. V ->. [ A / x ]_ ( B i^i ( C X. _V ) ) = ( [_ A / x ]_ B i^i ( [_ A / x ]_ C X.V ) ) ).
9:: ` |- ( B |`C ) = ( B i^i ( C X. V ) )
10:9: ` |- A. x ( B |`C ) = ( B i^i ( C X.V ) )
11:1,10: ` |- (. A e. V ->. [ A / x ]_ ( B |`C ) = [_ A / x ]_ ( B i^i ( C X.V ) ) ).
12:8,11: ` |- (. A e. V ->. [ A / x ]_ ( B |`C ) = ( [_ A / x ]_ B i^i ( [_ A / x ]_ C X.V ) ) ).
13:: ` |- ( [ A / x ]_ B |`[_ A / x ]_ C ) = ( [_ A / x ]_ B i^i ( [_ A / x ]_ C X.V ) )
14:12,13: ` |- (. A e. V ->. [ A / x ]_ ( B |`C ) = ( ` [_ A / x ]_ B |`[_ A / x ]_ C ) ).
qed:14: ` |- ( A e. V -> [_ A / x ]_ ( B |`C ) = ( ` [_ A / x ]_ B |`[_ A / x ]_ C ) )
(Contributed by Alan Sare, 10-Nov-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion csbresgVD ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↾ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 idn1 ⊢ (    𝐴 ∈ 𝑉    ▶    𝐴 ∈ 𝑉    )
2 csbconstg ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ V = V )
3 1 2 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ V = V    )
4 xpeq2 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ V = V → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × ⦋ 𝐴 / 𝑥 ⦌ V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) )
5 3 4 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × ⦋ 𝐴 / 𝑥 ⦌ V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V )    )
6 csbxp ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × ⦋ 𝐴 / 𝑥 ⦌ V )
7 6 a1i ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × ⦋ 𝐴 / 𝑥 ⦌ V ) )
8 1 7 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × ⦋ 𝐴 / 𝑥 ⦌ V )    )
9 eqeq2 ⊢ ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × ⦋ 𝐴 / 𝑥 ⦌ V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × ⦋ 𝐴 / 𝑥 ⦌ V ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) )
10 9 biimpd ⊢ ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × ⦋ 𝐴 / 𝑥 ⦌ V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × ⦋ 𝐴 / 𝑥 ⦌ V ) → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) )
11 5 8 10 e11 ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V )    )
12 ineq2 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) → ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) )
13 11 12 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) )    )
14 csbin ⊢ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) )
15 14 a1i ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) ) )
16 1 15 e1a ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) )    )
17 eqeq2 ⊢ ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) ) )
18 17 biimpd ⊢ ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐶 × V ) ) → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) ) )
19 13 16 18 e11 ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) )    )
20 df-res ⊢ ( 𝐵 ↾ 𝐶 ) = ( 𝐵 ∩ ( 𝐶 × V ) )
21 20 ax-gen ⊢ ∀ 𝑥 ( 𝐵 ↾ 𝐶 ) = ( 𝐵 ∩ ( 𝐶 × V ) )
22 csbeq2 ⊢ ( ∀ 𝑥 ( 𝐵 ↾ 𝐶 ) = ( 𝐵 ∩ ( 𝐶 × V ) ) → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) ) )
23 22 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ( 𝐵 ↾ 𝐶 ) = ( 𝐵 ∩ ( 𝐶 × V ) ) → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) ) ) )
24 1 21 23 e10 ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) )    )
25 eqeq2 ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) ) )
26 25 biimpd ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ∩ ( 𝐶 × V ) ) → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) ) )
27 19 24 26 e11 ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) )    )
28 df-res ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↾ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) )
29 eqeq2 ⊢ ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↾ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) → ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↾ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ↔ ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) ) )
30 29 biimprcd ⊢ ( ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) → ( ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↾ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ∩ ( ⦋ 𝐴 / 𝑥 ⦌ 𝐶 × V ) ) → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↾ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) ) )
31 27 28 30 e10 ⊢ (    𝐴 ∈ 𝑉    ▶    ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↾ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 )    )
32 31 in1 ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ( 𝐵 ↾ 𝐶 ) = ( ⦋ 𝐴 / 𝑥 ⦌ 𝐵 ↾ ⦋ 𝐴 / 𝑥 ⦌ 𝐶 ) )