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		reldmress	$⊢ Rel dom ↾_{𝑠}$
16	15	ovprc1	$⊢ \neg W \in V \to W ↾_{𝑠} A = \emptyset$
17	1 16	syl5eq	$⊢ \neg W \in V \to R = \emptyset$
18	17	fveq2d	$⊢ \neg W \in V \to E (R) = E (\emptyset)$
19	3	str0	$⊢ \emptyset = E (\emptyset)$
20	18 19	eqtr4di	$⊢ \neg W \in V \to E (R) = \emptyset$
21		fvprc	$⊢ \neg W \in V \to E (W) = \emptyset$
22	20 21	eqtr4d	$⊢ \neg W \in V \to E (R) = E (W)$
23	22	adantr	$⊢ (\neg W \in V \land A \in V) \to E (R) = E (W)$
24	14 23	pm2.61ian	$⊢ A \in V \to E (R) = E (W)$
25	2 24	eqtr4id	$⊢ A \in V \to C = E (R)$

Metamath Proof Explorer

Theorem resseqnbas

Proof