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	3	str0	⊢ ∅ = ( 𝐸 ‘ ∅ )
16	15	eqcomi	⊢ ( 𝐸 ‘ ∅ ) = ∅
17		reldmress	⊢ Rel dom ↾_s
18	16 1 17	oveqprc	⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ 𝑅 ) )
19	18	eqcomd	⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
20	19	adantr	⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
21	14 20	pm2.61ian	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
22	2 21	eqtr4id	⊢ ( 𝐴 ∈ 𝑉 → 𝐶 = ( 𝐸 ‘ 𝑅 ) )

Metamath Proof Explorer

Theorem resseqnbas

Proof