Theorem 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	⊢ 𝑅 = ( 𝑊 ↾s 𝐴 )
	resseqnbas.e	⊢ 𝐶 = ( 𝐸 ‘ 𝑊 )
	resseqnbas.f	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
	resseqnbas.n	⊢ ( 𝐸 ‘ ndx ) ≠ ( Base ‘ ndx )
Assertion	resseqnbas	⊢ ( 𝐴 ∈ 𝑉 → 𝐶 = ( 𝐸 ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		resseqnbas.r	⊢ 𝑅 = ( 𝑊 ↾s 𝐴 )
2		resseqnbas.e	⊢ 𝐶 = ( 𝐸 ‘ 𝑊 )
3		resseqnbas.f	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
4		resseqnbas.n	⊢ ( 𝐸 ‘ ndx ) ≠ ( Base ‘ ndx )
5		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6	1 5	ressid2	⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = 𝑊 )
7	6	fveq2d	⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
8	7	3expib	⊢ ( ( Base ‘ 𝑊 ) ⊆ 𝐴 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) )
9	1 5	ressval2	⊢ ( ( ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⟩ ) )
10	9	fveq2d	⊢ ( ( ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⟩ ) ) )
11	3 4	setsnid	⊢ ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⟩ ) )
12	10 11	eqtr4di	⊢ ( ( ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
13	12	3expib	⊢ ( ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) )
14	8 13	pm2.61i	⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
15		reldmress	⊢ Rel dom ↾s
16	15	ovprc1	⊢ ( ¬ 𝑊 ∈ V → ( 𝑊 ↾s 𝐴 ) = ∅ )
17	1 16	syl5eq	⊢ ( ¬ 𝑊 ∈ V → 𝑅 = ∅ )
18	17	fveq2d	⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ ∅ ) )
19	3	str0	⊢ ∅ = ( 𝐸 ‘ ∅ )
20	18 19	eqtr4di	⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑅 ) = ∅ )
21		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ∅ )
22	20 21	eqtr4d	⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
23	22	adantr	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
24	14 23	pm2.61ian	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
25	2 24	eqtr4id	⊢ ( 𝐴 ∈ 𝑉 → 𝐶 = ( 𝐸 ‘ 𝑅 ) )