Metamath Proof Explorer

Theorem ressval

Description: Value of structure restriction. (Contributed by Stefan O'Rear, 29-Nov-2014)

Ref Expression
Hypotheses ressbas.r ⊢ 𝑅 = ( 𝑊 ↾s 𝐴 )
ressbas.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
Assertion ressval ( ( 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → 𝑅 = if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) ) )

Proof

Step Hyp Ref Expression
1 ressbas.r ⊢ 𝑅 = ( 𝑊 ↾s 𝐴 )
2 ressbas.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
3 elex ⊢ ( 𝑊 ∈ 𝑋 → 𝑊 ∈ V )
4 elex ⊢ ( 𝐴 ∈ 𝑌 → 𝐴 ∈ V )
5 simpl ⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ V ) → 𝑊 ∈ V )
6 ovex ⊢ ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) ∈ V
7 ifcl ⊢ ( ( 𝑊 ∈ V ∧ ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) ∈ V ) → if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) ) ∈ V )
8 5 6 7 sylancl ⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ V ) → if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) ) ∈ V )
9 simpl ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = 𝐴 ) → 𝑤 = 𝑊 )
10 9 fveq2d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = 𝐴 ) → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
11 10 2 eqtr4di ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = 𝐴 ) → ( Base ‘ 𝑤 ) = 𝐵 )
12 simpr ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = 𝐴 ) → 𝑎 = 𝐴 )
13 11 12 sseq12d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = 𝐴 ) → ( ( Base ‘ 𝑤 ) ⊆ 𝑎 ↔ 𝐵 ⊆ 𝐴 ) )
14 12 11 ineq12d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = 𝐴 ) → ( 𝑎 ∩ ( Base ‘ 𝑤 ) ) = ( 𝐴 ∩ 𝐵 ) )
15 14 opeq2d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = 𝐴 ) → ⟨ ( Base ‘ ndx ) , ( 𝑎 ∩ ( Base ‘ 𝑤 ) ) ⟩ = ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ )
16 9 15 oveq12d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = 𝐴 ) → ( 𝑤 sSet ⟨ ( Base ‘ ndx ) , ( 𝑎 ∩ ( Base ‘ 𝑤 ) ) ⟩ ) = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) )
17 13 9 16 ifbieq12d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑎 = 𝐴 ) → if ( ( Base ‘ 𝑤 ) ⊆ 𝑎 , 𝑤 , ( 𝑤 sSet ⟨ ( Base ‘ ndx ) , ( 𝑎 ∩ ( Base ‘ 𝑤 ) ) ⟩ ) ) = if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) ) )
18 df-ress ⊢ ↾s = ( 𝑤 ∈ V , 𝑎 ∈ V ↦ if ( ( Base ‘ 𝑤 ) ⊆ 𝑎 , 𝑤 , ( 𝑤 sSet ⟨ ( Base ‘ ndx ) , ( 𝑎 ∩ ( Base ‘ 𝑤 ) ) ⟩ ) ) )
19 17 18 ovmpoga ⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ V ∧ if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) ) ∈ V ) → ( 𝑊 ↾s 𝐴 ) = if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) ) )
20 8 19 mpd3an3 ⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ V ) → ( 𝑊 ↾s 𝐴 ) = if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) ) )
21 3 4 20 syl2an ⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → ( 𝑊 ↾s 𝐴 ) = if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) ) )
22 1 21 syl5eq ⊢ ( ( 𝑊 ∈ 𝑋 ∧ 𝐴 ∈ 𝑌 ) → 𝑅 = if ( 𝐵 ⊆ 𝐴 , 𝑊 , ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) ) )