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 
|- R = ( S |`s A )
ressval3d.b 
|- B = ( Base ` S )
ressval3d.e 
|- E = ( Base ` ndx )
ressval3d.s 
|- ( ph -> S e. V )
ressval3d.f 
|- ( ph -> Fun S )
ressval3d.d 
|- ( ph -> E e. dom S )
ressval3d.u 
|- ( ph -> A C_ B )
Assertion ressval3d 
|- ( ph -> R = ( S sSet <. E , A >. ) )

Proof

Step Hyp Ref Expression
1 ressval3d.r 
 |-  R = ( S |`s A )
2 ressval3d.b 
 |-  B = ( Base ` S )
3 ressval3d.e 
 |-  E = ( Base ` ndx )
4 ressval3d.s 
 |-  ( ph -> S e. V )
5 ressval3d.f 
 |-  ( ph -> Fun S )
6 ressval3d.d 
 |-  ( ph -> E e. dom S )
7 ressval3d.u 
 |-  ( ph -> A C_ B )
8 sspss 
 |-  ( A C_ B <-> ( A C. B \/ A = B ) )
9 dfpss3 
 |-  ( A C. B <-> ( A C_ B /\ -. B C_ A ) )
10 9 orbi1i 
 |-  ( ( A C. B \/ A = B ) <-> ( ( A C_ B /\ -. B C_ A ) \/ A = B ) )
11 8 10 bitri 
 |-  ( A C_ B <-> ( ( A C_ B /\ -. B C_ A ) \/ A = B ) )
12 simplr 
 |-  ( ( ( A C_ B /\ -. B C_ A ) /\ ph ) -> -. B C_ A )
13 4 adantl 
 |-  ( ( ( A C_ B /\ -. B C_ A ) /\ ph ) -> S e. V )
14 simpl 
 |-  ( ( A C_ B /\ -. B C_ A ) -> A C_ B )
15 2 fvexi 
 |-  B e. _V
16 15 a1i 
 |-  ( ph -> B e. _V )
17 ssexg 
 |-  ( ( A C_ B /\ B e. _V ) -> A e. _V )
18 14 16 17 syl2an 
 |-  ( ( ( A C_ B /\ -. B C_ A ) /\ ph ) -> A e. _V )
19 1 2 ressval2 
 |-  ( ( -. B C_ A /\ S e. V /\ A e. _V ) -> R = ( S sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) )
20 12 13 18 19 syl3anc 
 |-  ( ( ( A C_ B /\ -. B C_ A ) /\ ph ) -> R = ( S sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) )
21 3 a1i 
 |-  ( ( ( A C_ B /\ -. B C_ A ) /\ ph ) -> E = ( Base ` ndx ) )
22 df-ss 
 |-  ( A C_ B <-> ( A i^i B ) = A )
23 22 biimpi 
 |-  ( A C_ B -> ( A i^i B ) = A )
24 23 eqcomd 
 |-  ( A C_ B -> A = ( A i^i B ) )
25 24 adantr 
 |-  ( ( A C_ B /\ -. B C_ A ) -> A = ( A i^i B ) )
26 25 adantr 
 |-  ( ( ( A C_ B /\ -. B C_ A ) /\ ph ) -> A = ( A i^i B ) )
27 21 26 opeq12d 
 |-  ( ( ( A C_ B /\ -. B C_ A ) /\ ph ) -> <. E , A >. = <. ( Base ` ndx ) , ( A i^i B ) >. )
28 27 eqcomd 
 |-  ( ( ( A C_ B /\ -. B C_ A ) /\ ph ) -> <. ( Base ` ndx ) , ( A i^i B ) >. = <. E , A >. )
29 28 oveq2d 
 |-  ( ( ( A C_ B /\ -. B C_ A ) /\ ph ) -> ( S sSet <. ( Base ` ndx ) , ( A i^i B ) >. ) = ( S sSet <. E , A >. ) )
30 20 29 eqtrd 
 |-  ( ( ( A C_ B /\ -. B C_ A ) /\ ph ) -> R = ( S sSet <. E , A >. ) )
31 30 ex 
 |-  ( ( A C_ B /\ -. B C_ A ) -> ( ph -> R = ( S sSet <. E , A >. ) ) )
32 1 a1i 
 |-  ( ( A = B /\ ph ) -> R = ( S |`s A ) )
33 oveq2 
 |-  ( A = B -> ( S |`s A ) = ( S |`s B ) )
34 33 adantr 
 |-  ( ( A = B /\ ph ) -> ( S |`s A ) = ( S |`s B ) )
35 4 adantl 
 |-  ( ( A = B /\ ph ) -> S e. V )
36 2 ressid 
 |-  ( S e. V -> ( S |`s B ) = S )
37 35 36 syl 
 |-  ( ( A = B /\ ph ) -> ( S |`s B ) = S )
38 32 34 37 3eqtrd 
 |-  ( ( A = B /\ ph ) -> R = S )
39 baseid 
 |-  Base = Slot ( Base ` ndx )
40 3 6 eqeltrrid 
 |-  ( ph -> ( Base ` ndx ) e. dom S )
41 39 4 5 40 setsidvald 
 |-  ( ph -> S = ( S sSet <. ( Base ` ndx ) , ( Base ` S ) >. ) )
42 41 adantl 
 |-  ( ( A = B /\ ph ) -> S = ( S sSet <. ( Base ` ndx ) , ( Base ` S ) >. ) )
43 3 a1i 
 |-  ( ( A = B /\ ph ) -> E = ( Base ` ndx ) )
44 simpl 
 |-  ( ( A = B /\ ph ) -> A = B )
45 44 2 eqtrdi 
 |-  ( ( A = B /\ ph ) -> A = ( Base ` S ) )
46 43 45 opeq12d 
 |-  ( ( A = B /\ ph ) -> <. E , A >. = <. ( Base ` ndx ) , ( Base ` S ) >. )
47 46 eqcomd 
 |-  ( ( A = B /\ ph ) -> <. ( Base ` ndx ) , ( Base ` S ) >. = <. E , A >. )
48 47 oveq2d 
 |-  ( ( A = B /\ ph ) -> ( S sSet <. ( Base ` ndx ) , ( Base ` S ) >. ) = ( S sSet <. E , A >. ) )
49 38 42 48 3eqtrd 
 |-  ( ( A = B /\ ph ) -> R = ( S sSet <. E , A >. ) )
50 49 ex 
 |-  ( A = B -> ( ph -> R = ( S sSet <. E , A >. ) ) )
51 31 50 jaoi 
 |-  ( ( ( A C_ B /\ -. B C_ A ) \/ A = B ) -> ( ph -> R = ( S sSet <. E , A >. ) ) )
52 11 51 sylbi 
 |-  ( A C_ B -> ( ph -> R = ( S sSet <. E , A >. ) ) )
53 7 52 mpcom 
 |-  ( ph -> R = ( S sSet <. E , A >. ) )