Metamath Proof Explorer

Theorem ressval3d

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

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 df-ss ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
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 df-base ⊢ Base = Slot 1
40 1nn ⊢ 1 ∈ ℕ
41 3 6 eqeltrrid ⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝑆 )
42 39 40 4 5 41 setsidvald ⊢ ( 𝜑 → 𝑆 = ( 𝑆 sSet ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ ) )
43 42 adantl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝑆 = ( 𝑆 sSet ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ ) )
44 3 a1i ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝐸 = ( Base ‘ ndx ) )
45 simpl ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝐴 = 𝐵 )
46 45 2 eqtrdi ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝐴 = ( Base ‘ 𝑆 ) )
47 44 46 opeq12d ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → ⟨ 𝐸 , 𝐴 ⟩ = ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ )
48 47 eqcomd ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ = ⟨ 𝐸 , 𝐴 ⟩ )
49 48 oveq2d ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → ( 𝑆 sSet ⟨ ( Base ‘ ndx ) , ( Base ‘ 𝑆 ) ⟩ ) = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) )
50 38 43 49 3eqtrd ⊢ ( ( 𝐴 = 𝐵 ∧ 𝜑 ) → 𝑅 = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) )
51 50 ex ⊢ ( 𝐴 = 𝐵 → ( 𝜑 → 𝑅 = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) ) )
52 31 51 jaoi ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ¬ 𝐵 ⊆ 𝐴 ) ∨ 𝐴 = 𝐵 ) → ( 𝜑 → 𝑅 = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) ) )
53 11 52 sylbi ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝜑 → 𝑅 = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) ) )
54 7 53 mpcom ⊢ ( 𝜑 → 𝑅 = ( 𝑆 sSet ⟨ 𝐸 , 𝐴 ⟩ ) )