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 .

		Ref	Expression
	Assertion	csbresgVD	$⊢ A \in V \to ⦋ A / x ⦌ ({B ↾}_{C}) = {⦋ A / x ⦌ B ↾}_{⦋ A / x ⦌ C}$

Proof

Step	Hyp	Ref	Expression
1		idn1	$⊢ (A \in V \to A \in V)$
2		csbconstg	$⊢ A \in V \to ⦋ A / x ⦌ V = V$
3	1 2	e1a	$⊢ (A \in V \to ⦋ A / x ⦌ V = V)$
4		xpeq2	$⊢ ⦋ A / x ⦌ V = V \to ⦋ A / x ⦌ C \times ⦋ A / x ⦌ V = ⦋ A / x ⦌ C \times V$
5	3 4	e1a	$⊢ (A \in V \to ⦋ A / x ⦌ C \times ⦋ A / x ⦌ V = ⦋ A / x ⦌ C \times V)$
6		csbxp	$⊢ ⦋ A / x ⦌ (C \times V) = ⦋ A / x ⦌ C \times ⦋ A / x ⦌ V$
7	6	a1i	$⊢ A \in V \to ⦋ A / x ⦌ (C \times V) = ⦋ A / x ⦌ C \times ⦋ A / x ⦌ V$
8	1 7	e1a	$⊢ (A \in V \to ⦋ A / x ⦌ (C \times V) = ⦋ A / x ⦌ C \times ⦋ A / x ⦌ V)$
9		eqeq2	$⊢ ⦋ A / x ⦌ C \times ⦋ A / x ⦌ V = ⦋ A / x ⦌ C \times V \to (⦋ A / x ⦌ (C \times V) = ⦋ A / x ⦌ C \times ⦋ A / x ⦌ V \leftrightarrow ⦋ A / x ⦌ (C \times V) = ⦋ A / x ⦌ C \times V)$
10	9	biimpd	$⊢ ⦋ A / x ⦌ C \times ⦋ A / x ⦌ V = ⦋ A / x ⦌ C \times V \to (⦋ A / x ⦌ (C \times V) = ⦋ A / x ⦌ C \times ⦋ A / x ⦌ V \to ⦋ A / x ⦌ (C \times V) = ⦋ A / x ⦌ C \times V)$
11	5 8 10	e11	$⊢ (A \in V \to ⦋ A / x ⦌ (C \times V) = ⦋ A / x ⦌ C \times V)$
12		ineq2	$⊢ ⦋ A / x ⦌ (C \times V) = ⦋ A / x ⦌ C \times V \to ⦋ A / x ⦌ B \cap ⦋ A / x ⦌ (C \times V) = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V)$
13	11 12	e1a	$⊢ (A \in V \to ⦋ A / x ⦌ B \cap ⦋ A / x ⦌ (C \times V) = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V))$
14		csbin	$⊢ ⦋ A / x ⦌ (B \cap (C \times V)) = ⦋ A / x ⦌ B \cap ⦋ A / x ⦌ (C \times V)$
15	14	a1i	$⊢ A \in V \to ⦋ A / x ⦌ (B \cap (C \times V)) = ⦋ A / x ⦌ B \cap ⦋ A / x ⦌ (C \times V)$
16	1 15	e1a	$⊢ (A \in V \to ⦋ A / x ⦌ (B \cap (C \times V)) = ⦋ A / x ⦌ B \cap ⦋ A / x ⦌ (C \times V))$
17		eqeq2	$⊢ ⦋ A / x ⦌ B \cap ⦋ A / x ⦌ (C \times V) = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V) \to (⦋ A / x ⦌ (B \cap (C \times V)) = ⦋ A / x ⦌ B \cap ⦋ A / x ⦌ (C \times V) \leftrightarrow ⦋ A / x ⦌ (B \cap (C \times V)) = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V))$
18	17	biimpd	$⊢ ⦋ A / x ⦌ B \cap ⦋ A / x ⦌ (C \times V) = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V) \to (⦋ A / x ⦌ (B \cap (C \times V)) = ⦋ A / x ⦌ B \cap ⦋ A / x ⦌ (C \times V) \to ⦋ A / x ⦌ (B \cap (C \times V)) = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V))$
19	13 16 18	e11	$⊢ (A \in V \to ⦋ A / x ⦌ (B \cap (C \times V)) = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V))$
20		df-res	$⊢ {B ↾}_{C} = B \cap (C \times V)$
21	20	ax-gen	$⊢ \forall x {B ↾}_{C} = B \cap (C \times V)$
22		csbeq2	$⊢ \forall x {B ↾}_{C} = B \cap (C \times V) \to ⦋ A / x ⦌ ({B ↾}_{C}) = ⦋ A / x ⦌ (B \cap (C \times V))$
23	22	a1i	$⊢ A \in V \to (\forall x {B ↾}_{C} = B \cap (C \times V) \to ⦋ A / x ⦌ ({B ↾}_{C}) = ⦋ A / x ⦌ (B \cap (C \times V)))$
24	1 21 23	e10	$⊢ (A \in V \to ⦋ A / x ⦌ ({B ↾}_{C}) = ⦋ A / x ⦌ (B \cap (C \times V)))$
25		eqeq2	$⊢ ⦋ A / x ⦌ (B \cap (C \times V)) = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V) \to (⦋ A / x ⦌ ({B ↾}_{C}) = ⦋ A / x ⦌ (B \cap (C \times V)) \leftrightarrow ⦋ A / x ⦌ ({B ↾}_{C}) = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V))$
26	25	biimpd	$⊢ ⦋ A / x ⦌ (B \cap (C \times V)) = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V) \to (⦋ A / x ⦌ ({B ↾}_{C}) = ⦋ A / x ⦌ (B \cap (C \times V)) \to ⦋ A / x ⦌ ({B ↾}_{C}) = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V))$
27	19 24 26	e11	$⊢ (A \in V \to ⦋ A / x ⦌ ({B ↾}_{C}) = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V))$
28		df-res	$⊢ {⦋ A / x ⦌ B ↾}_{⦋ A / x ⦌ C} = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V)$
29		eqeq2	$⊢ {⦋ A / x ⦌ B ↾}_{⦋ A / x ⦌ C} = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V) \to (⦋ A / x ⦌ ({B ↾}_{C}) = {⦋ A / x ⦌ B ↾}_{⦋ A / x ⦌ C} \leftrightarrow ⦋ A / x ⦌ ({B ↾}_{C}) = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V))$
30	29	biimprcd	$⊢ ⦋ A / x ⦌ ({B ↾}_{C}) = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V) \to ({⦋ A / x ⦌ B ↾}_{⦋ A / x ⦌ C} = ⦋ A / x ⦌ B \cap (⦋ A / x ⦌ C \times V) \to ⦋ A / x ⦌ ({B ↾}_{C}) = {⦋ A / x ⦌ B ↾}_{⦋ A / x ⦌ C})$
31	27 28 30	e10	$⊢ (A \in V \to ⦋ A / x ⦌ ({B ↾}_{C}) = {⦋ A / x ⦌ B ↾}_{⦋ A / x ⦌ C})$
32	31	in1	$⊢ A \in V \to ⦋ A / x ⦌ ({B ↾}_{C}) = {⦋ A / x ⦌ B ↾}_{⦋ A / x ⦌ C}$

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 ) )

Metamath Proof Explorer

Theorem csbresgVD

Proof