predres

Description: Predecessor class is unaffected by restriction to the base class. (Contributed by Scott Fenton, 25-Nov-2024)

		Ref	Expression
	Assertion	predres	$⊢ Pred (R, A, X) = Pred (({R ↾}_{A}), A, X)$

Proof

Step	Hyp	Ref	Expression
1		ssrab2	$⊢ \{y \in A \| y R X\} \subseteq A$
2		sseqin2	$⊢ \{y \in A \| y R X\} \subseteq A \leftrightarrow A \cap \{y \in A \| y R X\} = \{y \in A \| y R X\}$
3	1 2	mpbi	$⊢ A \cap \{y \in A \| y R X\} = \{y \in A \| y R X\}$
4		dfrab2	$⊢ \{y \in A \| y R X\} = \{y \| y R X\} \cap A$
5	3 4	eqtr2i	$⊢ \{y \| y R X\} \cap A = A \cap \{y \in A \| y R X\}$
6		iniseg	$⊢ X \in V \to R^{-1} [\{X\}] = \{y \| y R X\}$
7	6	ineq2d	$⊢ X \in V \to A \cap R^{-1} [\{X\}] = A \cap \{y \| y R X\}$
8		incom	$⊢ A \cap \{y \| y R X\} = \{y \| y R X\} \cap A$
9	7 8	eqtrdi	$⊢ X \in V \to A \cap R^{-1} [\{X\}] = \{y \| y R X\} \cap A$
10		iniseg	$⊢ X \in V \to {({R ↾}_{A})}^{-1} [\{X\}] = \{y \| y ({R ↾}_{A}) X\}$
11		brres	$⊢ X \in V \to (y ({R ↾}_{A}) X \leftrightarrow (y \in A \land y R X))$
12	11	abbidv	$⊢ X \in V \to \{y \| y ({R ↾}_{A}) X\} = \{y \| (y \in A \land y R X)\}$
13		df-rab	$⊢ \{y \in A \| y R X\} = \{y \| (y \in A \land y R X)\}$
14	12 13	eqtr4di	$⊢ X \in V \to \{y \| y ({R ↾}_{A}) X\} = \{y \in A \| y R X\}$
15	10 14	eqtrd	$⊢ X \in V \to {({R ↾}_{A})}^{-1} [\{X\}] = \{y \in A \| y R X\}$
16	15	ineq2d	$⊢ X \in V \to A \cap {({R ↾}_{A})}^{-1} [\{X\}] = A \cap \{y \in A \| y R X\}$
17	5 9 16	3eqtr4a	$⊢ X \in V \to A \cap R^{-1} [\{X\}] = A \cap {({R ↾}_{A})}^{-1} [\{X\}]$
18		df-pred	$⊢ Pred (R, A, X) = A \cap R^{-1} [\{X\}]$
19		df-pred	$⊢ Pred (({R ↾}_{A}), A, X) = A \cap {({R ↾}_{A})}^{-1} [\{X\}]$
20	17 18 19	3eqtr4g	$⊢ X \in V \to Pred (R, A, X) = Pred (({R ↾}_{A}), A, X)$
21		predprc	$⊢ \neg X \in V \to Pred (R, A, X) = \emptyset$
22		predprc	$⊢ \neg X \in V \to Pred (({R ↾}_{A}), A, X) = \emptyset$
23	21 22	eqtr4d	$⊢ \neg X \in V \to Pred (R, A, X) = Pred (({R ↾}_{A}), A, X)$
24	20 23	pm2.61i	$⊢ Pred (R, A, X) = Pred (({R ↾}_{A}), A, X)$

Metamath Proof Explorer

Theorem predres

Proof