Metamath Proof Explorer

Theorem ressress

Description: Restriction composition law. (Contributed by Stefan O'Rear, 29-Nov-2014) (Proof shortened by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion ressress ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simplr ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 )
2 simpr1 ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → 𝑊 ∈ V )
3 simpr2 ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → 𝐴 ∈ 𝑋 )
4 eqid ⊢ ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s 𝐴 )
5 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
6 4 5 ressval2 ⊢ ( ( ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ) → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⟩ ) )
7 1 2 3 6 syl3anc ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⟩ ) )
8 inass ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) = ( 𝐴 ∩ ( 𝐵 ∩ ( Base ‘ 𝑊 ) ) )
9 in12 ⊢ ( 𝐴 ∩ ( 𝐵 ∩ ( Base ‘ 𝑊 ) ) ) = ( 𝐵 ∩ ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) )
10 8 9 eqtri ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) = ( 𝐵 ∩ ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) )
11 4 5 ressbas ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) = ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) )
12 3 11 syl ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) = ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) )
13 12 ineq2d ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐵 ∩ ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ) = ( 𝐵 ∩ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) )
14 10 13 syl5req ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐵 ∩ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) = ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) )
15 14 opeq2d ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ⟩ = ⟨ ( Base ‘ ndx ) , ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ⟩ )
16 7 15 oveq12d ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝑊 ↾s 𝐴 ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ⟩ ) = ( ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⟩ ) sSet ⟨ ( Base ‘ ndx ) , ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ⟩ ) )
17 fvex ⊢ ( Base ‘ 𝑊 ) ∈ V
18 17 inex2 ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ∈ V
19 setsabs ⊢ ( ( 𝑊 ∈ V ∧ ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ∈ V ) → ( ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⟩ ) sSet ⟨ ( Base ‘ ndx ) , ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ⟩ ) = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ⟩ ) )
20 2 18 19 sylancl ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⟩ ) sSet ⟨ ( Base ‘ ndx ) , ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ⟩ ) = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ⟩ ) )
21 16 20 eqtrd ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝑊 ↾s 𝐴 ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ⟩ ) = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ⟩ ) )
22 simpll ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 )
23 ovexd ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑊 ↾s 𝐴 ) ∈ V )
24 simpr3 ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → 𝐵 ∈ 𝑌 )
25 eqid ⊢ ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 )
26 eqid ⊢ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) = ( Base ‘ ( 𝑊 ↾s 𝐴 ) )
27 25 26 ressval2 ⊢ ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝑊 ↾s 𝐴 ) ∈ V ∧ 𝐵 ∈ 𝑌 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( ( 𝑊 ↾s 𝐴 ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ⟩ ) )
28 22 23 24 27 syl3anc ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( ( 𝑊 ↾s 𝐴 ) sSet ⟨ ( Base ‘ ndx ) , ( 𝐵 ∩ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ) ⟩ ) )
29 inss1 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
30 sstr ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ ( 𝐴 ∩ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ) → ( Base ‘ 𝑊 ) ⊆ 𝐴 )
31 29 30 mpan2 ⊢ ( ( Base ‘ 𝑊 ) ⊆ ( 𝐴 ∩ 𝐵 ) → ( Base ‘ 𝑊 ) ⊆ 𝐴 )
32 1 31 nsyl ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ¬ ( Base ‘ 𝑊 ) ⊆ ( 𝐴 ∩ 𝐵 ) )
33 inex1g ⊢ ( 𝐴 ∈ 𝑋 → ( 𝐴 ∩ 𝐵 ) ∈ V )
34 3 33 syl ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ V )
35 eqid ⊢ ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) )
36 35 5 ressval2 ⊢ ( ( ¬ ( Base ‘ 𝑊 ) ⊆ ( 𝐴 ∩ 𝐵 ) ∧ 𝑊 ∈ V ∧ ( 𝐴 ∩ 𝐵 ) ∈ V ) → ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ⟩ ) )
37 32 2 34 36 syl3anc ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ⟩ ) )
38 21 28 37 3eqtr4d ⊢ ( ( ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ) ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
39 38 exp31 ⊢ ( ¬ ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 → ( ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) ) ) )
40 ovex ⊢ ( 𝑊 ↾s 𝐴 ) ∈ V
41 25 26 ressid2 ⊢ ( ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝑊 ↾s 𝐴 ) ∈ V ∧ 𝐵 ∈ 𝑌 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s 𝐴 ) )
42 40 41 mp3an2 ⊢ ( ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ 𝐵 ∈ 𝑌 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s 𝐴 ) )
43 42 3ad2antr3 ⊢ ( ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s 𝐴 ) )
44 in32 ⊢ ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) = ( ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ∩ 𝐵 )
45 simpr2 ⊢ ( ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → 𝐴 ∈ 𝑋 )
46 45 11 syl ⊢ ( ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) = ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) )
47 simpl ⊢ ( ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 )
48 46 47 eqsstrd ⊢ ( ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⊆ 𝐵 )
49 df-ss ⊢ ( ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⊆ 𝐵 ↔ ( ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ∩ 𝐵 ) = ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) )
50 48 49 sylib ⊢ ( ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ∩ 𝐵 ) = ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) )
51 44 50 syl5req ⊢ ( ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) = ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) )
52 51 oveq2d ⊢ ( ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑊 ↾s ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ) = ( 𝑊 ↾s ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ) )
53 5 ressinbas ⊢ ( 𝐴 ∈ 𝑋 → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ) )
54 45 53 syl ⊢ ( ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ) )
55 5 ressinbas ⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ V → ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = ( 𝑊 ↾s ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ) )
56 45 33 55 3syl ⊢ ( ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = ( 𝑊 ↾s ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ) )
57 52 54 56 3eqtr4d ⊢ ( ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑊 ↾s 𝐴 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
58 43 57 eqtrd ⊢ ( ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
59 58 ex ⊢ ( ( Base ‘ ( 𝑊 ↾s 𝐴 ) ) ⊆ 𝐵 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) ) )
60 4 5 ressid2 ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ) → ( 𝑊 ↾s 𝐴 ) = 𝑊 )
61 60 3adant3r3 ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑊 ↾s 𝐴 ) = 𝑊 )
62 61 oveq1d ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s 𝐵 ) )
63 inss2 ⊢ ( 𝐵 ∩ ( Base ‘ 𝑊 ) ) ⊆ ( Base ‘ 𝑊 )
64 simpl ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( Base ‘ 𝑊 ) ⊆ 𝐴 )
65 63 64 sstrid ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐵 ∩ ( Base ‘ 𝑊 ) ) ⊆ 𝐴 )
66 sseqin2 ⊢ ( ( 𝐵 ∩ ( Base ‘ 𝑊 ) ) ⊆ 𝐴 ↔ ( 𝐴 ∩ ( 𝐵 ∩ ( Base ‘ 𝑊 ) ) ) = ( 𝐵 ∩ ( Base ‘ 𝑊 ) ) )
67 65 66 sylib ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐴 ∩ ( 𝐵 ∩ ( Base ‘ 𝑊 ) ) ) = ( 𝐵 ∩ ( Base ‘ 𝑊 ) ) )
68 8 67 syl5req ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝐵 ∩ ( Base ‘ 𝑊 ) ) = ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) )
69 68 oveq2d ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑊 ↾s ( 𝐵 ∩ ( Base ‘ 𝑊 ) ) ) = ( 𝑊 ↾s ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ) )
70 simpr3 ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → 𝐵 ∈ 𝑌 )
71 5 ressinbas ⊢ ( 𝐵 ∈ 𝑌 → ( 𝑊 ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐵 ∩ ( Base ‘ 𝑊 ) ) ) )
72 70 71 syl ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑊 ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐵 ∩ ( Base ‘ 𝑊 ) ) ) )
73 simpr2 ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → 𝐴 ∈ 𝑋 )
74 73 33 55 3syl ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = ( 𝑊 ↾s ( ( 𝐴 ∩ 𝐵 ) ∩ ( Base ‘ 𝑊 ) ) ) )
75 69 72 74 3eqtr4d ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑊 ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
76 62 75 eqtrd ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
77 76 ex ⊢ ( ( Base ‘ 𝑊 ) ⊆ 𝐴 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) ) )
78 39 59 77 pm2.61ii ⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
79 78 3expib ⊢ ( 𝑊 ∈ V → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) ) )
80 ress0 ⊢ ( ∅ ↾s 𝐵 ) = ∅
81 reldmress ⊢ Rel dom ↾s
82 81 ovprc1 ⊢ ( ¬ 𝑊 ∈ V → ( 𝑊 ↾s 𝐴 ) = ∅ )
83 82 oveq1d ⊢ ( ¬ 𝑊 ∈ V → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( ∅ ↾s 𝐵 ) )
84 81 ovprc1 ⊢ ( ¬ 𝑊 ∈ V → ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) = ∅ )
85 80 83 84 3eqtr4a ⊢ ( ¬ 𝑊 ∈ V → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )
86 85 a1d ⊢ ( ¬ 𝑊 ∈ V → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) ) )
87 79 86 pm2.61i ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ( 𝑊 ↾s 𝐴 ) ↾s 𝐵 ) = ( 𝑊 ↾s ( 𝐴 ∩ 𝐵 ) ) )