Metamath Proof Explorer


Theorem ressbasssg

Description: The base set of a restriction to A is a subset of A and the base set B of the original structure. (Contributed by SN, 10-Jan-2025)

Ref Expression
Hypotheses ressbas.r 𝑅 = ( 𝑊s 𝐴 )
ressbas.b 𝐵 = ( Base ‘ 𝑊 )
Assertion ressbasssg ( Base ‘ 𝑅 ) ⊆ ( 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 ressbas.r 𝑅 = ( 𝑊s 𝐴 )
2 ressbas.b 𝐵 = ( Base ‘ 𝑊 )
3 1 2 ressbas ( 𝐴 ∈ V → ( 𝐴𝐵 ) = ( Base ‘ 𝑅 ) )
4 ssid ( 𝐴𝐵 ) ⊆ ( 𝐴𝐵 )
5 3 4 eqsstrrdi ( 𝐴 ∈ V → ( Base ‘ 𝑅 ) ⊆ ( 𝐴𝐵 ) )
6 reldmress Rel dom ↾s
7 6 ovprc2 ( ¬ 𝐴 ∈ V → ( 𝑊s 𝐴 ) = ∅ )
8 1 7 eqtrid ( ¬ 𝐴 ∈ V → 𝑅 = ∅ )
9 8 fveq2d ( ¬ 𝐴 ∈ V → ( Base ‘ 𝑅 ) = ( Base ‘ ∅ ) )
10 base0 ∅ = ( Base ‘ ∅ )
11 0ss ∅ ⊆ ( 𝐴𝐵 )
12 10 11 eqsstrri ( Base ‘ ∅ ) ⊆ ( 𝐴𝐵 )
13 9 12 eqsstrdi ( ¬ 𝐴 ∈ V → ( Base ‘ 𝑅 ) ⊆ ( 𝐴𝐵 ) )
14 5 13 pm2.61i ( Base ‘ 𝑅 ) ⊆ ( 𝐴𝐵 )