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

Metamath Proof Explorer

Theorem ressval3d

Description: Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020) (Revised by AV, 3-Jul-2022) (Proof shortened by AV, 17-Oct-2024)

Ref Expression
Hypotheses ressval3d.r ⊢ 𝑅 = ( 𝑆 ↾s 𝐴 )
ressval3d.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
ressval3d.e ⊢ 𝐸 = ( Base ‘ ndx )
ressval3d.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
ressval3d.f ⊢ ( 𝜑 → Fun 𝑆 )
ressval3d.d ⊢ ( 𝜑 → 𝐸 ∈ dom 𝑆 )
ressval3d.u ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion ressval3d ( 𝜑 → 𝑅 = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) )

Proof

Step Hyp Ref Expression
1 ressval3d.r ⊢ 𝑅 = ( 𝑆 ↾s 𝐴 )
2 ressval3d.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 ressval3d.e ⊢ 𝐸 = ( Base ‘ ndx )
4 ressval3d.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
5 ressval3d.f ⊢ ( 𝜑 → Fun 𝑆 )
6 ressval3d.d ⊢ ( 𝜑 → 𝐸 ∈ dom 𝑆 )
7 ressval3d.u ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
8 sspss ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) )
9 dfpss3 ⊢ ( 𝐴 ⊊ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) )
10 9 orbi1i ⊢ ( ( 𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ) ↔ ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∨ 𝐴 = 𝐵 ) )
11 8 10 bitri ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∨ 𝐴 = 𝐵 ) )
12 simplr ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝜑 ) → ¬ 𝐵 ⊆ 𝐴 )
13 4 adantl ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝜑 ) → 𝑆 ∈ 𝑉 )
14 simpl ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) → 𝐴 ⊆ 𝐵 )
15 2 fvexi ⊢ 𝐵 ∈ V
16 15 a1i ⊢ ( 𝜑 → 𝐵 ∈ V )
17 ssexg ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ V ) → 𝐴 ∈ V )
18 14 16 17 syl2an ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝜑 ) → 𝐴 ∈ V )
19 1 2 ressval2 ⊢ ( ( ¬ 𝐵 ⊆ 𝐴 ∧ 𝑆 ∈ 𝑉 ∧ 𝐴 ∈ V ) → 𝑅 = ( 𝑆 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) )
20 12 13 18 19 syl3anc ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝜑 ) → 𝑅 = ( 𝑆 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) )
21 3 a1i ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝜑 ) → 𝐸 = ( Base ‘ ndx ) )
22 dfss2 ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
23 22 biimpi ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∩ 𝐵 ) = 𝐴 )
24 23 eqcomd ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( 𝐴 ∩ 𝐵 ) )
25 24 adantr ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) → 𝐴 = ( 𝐴 ∩ 𝐵 ) )
26 25 adantr ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝜑 ) → 𝐴 = ( 𝐴 ∩ 𝐵 ) )
27 21 26 opeq12d ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝜑 ) → ⟨ 𝐸 , 𝐴 ⟩ = ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ )
28 27 eqcomd ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝜑 ) → ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ = ⟨ 𝐸 , 𝐴 ⟩ )
29 28 oveq2d ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝜑 ) → ( 𝑆 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ 𝐵 ) ⟩ ) = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) )
30 20 29 eqtrd ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∧ 𝜑 ) → 𝑅 = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) )
31 30 ex ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) → ( 𝜑 → 𝑅 = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) ) )
32 1 a1i ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝑅 = ( 𝑆 ↾s 𝐴 ) )
33 oveq2 ⊢ ( 𝐴 = 𝐵 → ( 𝑆 ↾s 𝐴 ) = ( 𝑆 ↾s 𝐵 ) )
34 33 adantr ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → ( 𝑆 ↾s 𝐴 ) = ( 𝑆 ↾s 𝐵 ) )
35 4 adantl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝑆 ∈ 𝑉 )
36 2 ressid ⊢ ( 𝑆 ∈ 𝑉 → ( 𝑆 ↾s 𝐵 ) = 𝑆 )
37 35 36 syl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → ( 𝑆 ↾s 𝐵 ) = 𝑆 )
38 32 34 37 3eqtrd ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝑅 = 𝑆 )
39 baseid ⊢ Base = Slot ( Base ‘ ndx )
40 3 6 eqeltrrid ⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝑆 )
41 39 4 5 40 setsidvald ⊢ ( 𝜑 → 𝑆 = ( 𝑆 sSet ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ ) )
42 41 adantl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝑆 = ( 𝑆 sSet ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ ) )
43 3 a1i ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝐸 = ( Base ‘ ndx ) )
44 simpl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝐴 = 𝐵 )
45 44 2 eqtrdi ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝐴 = ( Base ‘ 𝑆 ) )
46 43 45 opeq12d ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → ⟨ 𝐸 , 𝐴 ⟩ = ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ )
47 46 eqcomd ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ = ⟨ 𝐸 , 𝐴 ⟩ )
48 47 oveq2d ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → ( 𝑆 sSet ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ ) = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) )
49 38 42 48 3eqtrd ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝑅 = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) )
50 49 ex ⊢ ( 𝐴 = 𝐵 → ( 𝜑 → 𝑅 = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) ) )
51 31 50 jaoi ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∨ 𝐴 = 𝐵 ) → ( 𝜑 → 𝑅 = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) ) )
52 11 51 sylbi ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝜑 → 𝑅 = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) ) )
53 7 52 mpcom ⊢ ( 𝜑 → 𝑅 = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) )