This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑅 ) ⊆ ( 𝐴 ∩ 𝐵 )