resseqnbas

Description: The components of an extensible structure except the base set remain unchanged on a structure restriction. (Contributed by Mario Carneiro, 26-Nov-2014) (Revised by Mario Carneiro, 2-Dec-2014) (Revised by AV, 19-Oct-2024)

	Ref	Expression
Hypotheses	resseqnbas.r	$⊢ R = W ↾_{𝑠} A$
	resseqnbas.e	$⊢ C = E (W)$
	resseqnbas.f	$⊢ E = Slot E (ndx)$
	resseqnbas.n	$⊢ E (ndx) \neq {Base}_{ndx}$
Assertion	resseqnbas	$⊢ A \in V \to C = E (R)$

Proof

Step	Hyp	Ref	Expression
1		resseqnbas.r	$⊢ R = W ↾_{𝑠} A$
2		resseqnbas.e	$⊢ C = E (W)$
3		resseqnbas.f	$⊢ E = Slot E (ndx)$
4		resseqnbas.n	$⊢ E (ndx) \neq {Base}_{ndx}$
5		eqid	$⊢ {Base}_{W} = {Base}_{W}$
6	1 5	ressid2	$⊢ ({Base}_{W} \subseteq A \land W \in V \land A \in V) \to R = W$
7	6	fveq2d	$⊢ ({Base}_{W} \subseteq A \land W \in V \land A \in V) \to E (R) = E (W)$
8	7	3expib	$⊢ {Base}_{W} \subseteq A \to ((W \in V \land A \in V) \to E (R) = E (W))$
9	1 5	ressval2	$⊢ (\neg {Base}_{W} \subseteq A \land W \in V \land A \in V) \to R = W sSet ⟨{Base}_{ndx}, A \cap {Base}_{W}⟩$
10	9	fveq2d	$⊢ (\neg {Base}_{W} \subseteq A \land W \in V \land A \in V) \to E (R) = E (W sSet ⟨{Base}_{ndx}, A \cap {Base}_{W}⟩)$
11	3 4	setsnid	$⊢ E (W) = E (W sSet ⟨{Base}_{ndx}, A \cap {Base}_{W}⟩)$
12	10 11	eqtr4di	$⊢ (\neg {Base}_{W} \subseteq A \land W \in V \land A \in V) \to E (R) = E (W)$
13	12	3expib	$⊢ \neg {Base}_{W} \subseteq A \to ((W \in V \land A \in V) \to E (R) = E (W))$
14	8 13	pm2.61i	$⊢ (W \in V \land A \in V) \to E (R) = E (W)$
15	3	str0	$⊢ \emptyset = E (\emptyset)$
16	15	eqcomi	$⊢ E (\emptyset) = \emptyset$
17		reldmress	$⊢ Rel dom ↾_{𝑠}$
18	16 1 17	oveqprc	$⊢ \neg W \in V \to E (W) = E (R)$
19	18	eqcomd	$⊢ \neg W \in V \to E (R) = E (W)$
20	19	adantr	$⊢ (\neg W \in V \land A \in V) \to E (R) = E (W)$
21	14 20	pm2.61ian	$⊢ A \in V \to E (R) = E (W)$
22	2 21	eqtr4id	$⊢ A \in V \to C = E (R)$

Metamath Proof Explorer

Theorem resseqnbas

Proof