Metamath Proof Explorer

Theorem ressinbas

Description: Restriction only cares about the part of the second set which intersects the base of the first. (Contributed by Stefan O'Rear, 29-Nov-2014)

Ref Expression
Hypothesis ressid.1 ⊢ 𝐵 = ( Base ‘ 𝑊 )
Assertion ressinbas ( 𝐴 ∈ 𝑋 → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ressid.1 ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 elex ⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ V )
3 eqid ⊢ ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s 𝐴 )
4 3 1 ressid2 ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑊 ↾s 𝐴 ) = 𝑊 )
5 ssid ⊢ 𝐵 ⊆ 𝐵
6 incom ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
7 df-ss ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∩ 𝐴 ) = 𝐵 )
8 7 biimpi ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐵 ∩ 𝐴 ) = 𝐵 )
9 6 8 syl5eq ⊢ ( 𝐵 ⊆ 𝐴 → ( 𝐴 ∩ 𝐵 ) = 𝐵 )
10 5 9 sseqtrrid ⊢ ( 𝐵 ⊆ 𝐴 → 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) )
11 elex ⊢ ( 𝑊 ∈ V → 𝑊 ∈ V )
12 inex1g ⊢ ( 𝐴 ∈ V → ( 𝐴 ∩ 𝐵 ) ∈ V )
13 eqid ⊢ ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) )
14 13 1 ressid2 ⊢ ( ( 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) ∧ 𝑊 ∈ V ∧ ( 𝐴 ∩ 𝐵 ) ∈ V ) → ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = 𝑊 )
15 10 11 12 14 syl3an ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = 𝑊 )
16 4 15 eqtr4d ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
17 16 3expb ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ V ) ) → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
18 inass ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐵 ) = ( 𝐴 ∩ ( 𝐵 ∩ 𝐵 ) )
19 inidm ⊢ ( 𝐵 ∩ 𝐵 ) = 𝐵
20 19 ineq2i ⊢ ( 𝐴 ∩ ( 𝐵 ∩ 𝐵 ) ) = ( 𝐴 ∩ 𝐵 )
21 18 20 eqtr2i ⊢ ( 𝐴 ∩ 𝐵 ) = ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐵 )
22 21 opeq2i ⊢ ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ = ⟨ ( Base ‘ ndx ) , ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐵 ) ⟩
23 22 oveq2i ⊢ ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐵 ) ⟩ )
24 3 1 ressval2 ⊢ ( ( ¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) )
25 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
26 sstr ⊢ ( ( 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → 𝐵 ⊆ 𝐴 )
27 25 26 mpan2 ⊢ ( 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) → 𝐵 ⊆ 𝐴 )
28 27 con3i ⊢ ( ¬ 𝐵 ⊆ 𝐴 → ¬ 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) )
29 13 1 ressval2 ⊢ ( ( ¬ 𝐵 ⊆ ( 𝐴 ∩ 𝐵 ) ∧ 𝑊 ∈ V ∧ ( 𝐴 ∩ 𝐵 ) ∈ V ) → ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐵 ) ⟩ ) )
30 28 11 12 29 syl3an ⊢ ( ( ¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐵 ) ⟩ ) )
31 23 24 30 3eqtr4a ⊢ ( ( ¬ 𝐵 ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
32 31 3expb ⊢ ( ( ¬ 𝐵 ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ V ) ) → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
33 17 32 pm2.61ian ⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
34 reldmress ⊢ Rel dom ↾s
35 34 ovprc1 ⊢ ( ¬ 𝑊 ∈ V → ( 𝑊 ↾s 𝐴 ) = ∅ )
36 34 ovprc1 ⊢ ( ¬ 𝑊 ∈ V → ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = ∅ )
37 35 36 eqtr4d ⊢ ( ¬ 𝑊 ∈ V → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
38 37 adantr ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
39 33 38 pm2.61ian ⊢ ( 𝐴 ∈ V → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
40 2 39 syl ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )