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

Metamath Proof Explorer

Theorem suppssov1

Description: Formula building theorem for support restrictions: operator with left annihilator. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 28-May-2019) (Proof shortened by SN, 11-Apr-2025)

Ref Expression
Hypotheses suppssov1.s 
|- ( ph -> ( ( x e. D |-> A ) supp Y ) C_ L )
suppssov1.o 
|- ( ( ph /\ v e. R ) -> ( Y O v ) = Z )
suppssov1.a 
|- ( ( ph /\ x e. D ) -> A e. V )
suppssov1.b 
|- ( ( ph /\ x e. D ) -> B e. R )
suppssov1.y 
|- ( ph -> Y e. W )
Assertion suppssov1 
|- ( ph -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ L )

Proof

Step Hyp Ref Expression
1 suppssov1.s 
 |-  ( ph -> ( ( x e. D |-> A ) supp Y ) C_ L )
2 suppssov1.o 
 |-  ( ( ph /\ v e. R ) -> ( Y O v ) = Z )
3 suppssov1.a 
 |-  ( ( ph /\ x e. D ) -> A e. V )
4 suppssov1.b 
 |-  ( ( ph /\ x e. D ) -> B e. R )
5 suppssov1.y 
 |-  ( ph -> Y e. W )
6 3 elexd 
 |-  ( ( ph /\ x e. D ) -> A e. _V )
7 6 adantlr 
 |-  ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) -> A e. _V )
8 7 adantr 
 |-  ( ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) /\ ( A O B ) e. ( _V \ { Z } ) ) -> A e. _V )
9 oveq2 
 |-  ( v = B -> ( Y O v ) = ( Y O B ) )
10 9 eqeq1d 
 |-  ( v = B -> ( ( Y O v ) = Z <-> ( Y O B ) = Z ) )
11 2 ralrimiva 
 |-  ( ph -> A. v e. R ( Y O v ) = Z )
12 11 ad2antrr 
 |-  ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) -> A. v e. R ( Y O v ) = Z )
13 4 adantlr 
 |-  ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) -> B e. R )
14 10 12 13 rspcdva 
 |-  ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) -> ( Y O B ) = Z )
15 oveq1 
 |-  ( A = Y -> ( A O B ) = ( Y O B ) )
16 15 eqeq1d 
 |-  ( A = Y -> ( ( A O B ) = Z <-> ( Y O B ) = Z ) )
17 14 16 syl5ibrcom 
 |-  ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) -> ( A = Y -> ( A O B ) = Z ) )
18 17 necon3d 
 |-  ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) -> ( ( A O B ) =/= Z -> A =/= Y ) )
19 eldifsni 
 |-  ( ( A O B ) e. ( _V \ { Z } ) -> ( A O B ) =/= Z )
20 18 19 impel 
 |-  ( ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) /\ ( A O B ) e. ( _V \ { Z } ) ) -> A =/= Y )
21 eldifsn 
 |-  ( A e. ( _V \ { Y } ) <-> ( A e. _V /\ A =/= Y ) )
22 8 20 21 sylanbrc 
 |-  ( ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) /\ ( A O B ) e. ( _V \ { Z } ) ) -> A e. ( _V \ { Y } ) )
23 22 ex 
 |-  ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) -> ( ( A O B ) e. ( _V \ { Z } ) -> A e. ( _V \ { Y } ) ) )
24 23 ss2rabdv 
 |-  ( ( ph /\ ( D e. _V /\ Z e. _V ) ) -> { x e. D | ( A O B ) e. ( _V \ { Z } ) } C_ { x e. D | A e. ( _V \ { Y } ) } )
25 eqid 
 |-  ( x e. D |-> ( A O B ) ) = ( x e. D |-> ( A O B ) )
26 simprl 
 |-  ( ( ph /\ ( D e. _V /\ Z e. _V ) ) -> D e. _V )
27 simprr 
 |-  ( ( ph /\ ( D e. _V /\ Z e. _V ) ) -> Z e. _V )
28 25 26 27 mptsuppdifd 
 |-  ( ( ph /\ ( D e. _V /\ Z e. _V ) ) -> ( ( x e. D |-> ( A O B ) ) supp Z ) = { x e. D | ( A O B ) e. ( _V \ { Z } ) } )
29 eqid 
 |-  ( x e. D |-> A ) = ( x e. D |-> A )
30 5 adantr 
 |-  ( ( ph /\ ( D e. _V /\ Z e. _V ) ) -> Y e. W )
31 29 26 30 mptsuppdifd 
 |-  ( ( ph /\ ( D e. _V /\ Z e. _V ) ) -> ( ( x e. D |-> A ) supp Y ) = { x e. D | A e. ( _V \ { Y } ) } )
32 24 28 31 3sstr4d 
 |-  ( ( ph /\ ( D e. _V /\ Z e. _V ) ) -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ ( ( x e. D |-> A ) supp Y ) )
33 1 adantr 
 |-  ( ( ph /\ ( D e. _V /\ Z e. _V ) ) -> ( ( x e. D |-> A ) supp Y ) C_ L )
34 32 33 sstrd 
 |-  ( ( ph /\ ( D e. _V /\ Z e. _V ) ) -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ L )
35 mptexg 
 |-  ( D e. _V -> ( x e. D |-> ( A O B ) ) e. _V )
36 ovex 
 |-  ( A O B ) e. _V
37 36 rgenw 
 |-  A. x e. D ( A O B ) e. _V
38 dmmptg 
 |-  ( A. x e. D ( A O B ) e. _V -> dom ( x e. D |-> ( A O B ) ) = D )
39 37 38 ax-mp 
 |-  dom ( x e. D |-> ( A O B ) ) = D
40 dmexg 
 |-  ( ( x e. D |-> ( A O B ) ) e. _V -> dom ( x e. D |-> ( A O B ) ) e. _V )
41 39 40 eqeltrrid 
 |-  ( ( x e. D |-> ( A O B ) ) e. _V -> D e. _V )
42 35 41 impbii 
 |-  ( D e. _V <-> ( x e. D |-> ( A O B ) ) e. _V )
43 42 anbi1i 
 |-  ( ( D e. _V /\ Z e. _V ) <-> ( ( x e. D |-> ( A O B ) ) e. _V /\ Z e. _V ) )
44 supp0prc 
 |-  ( -. ( ( x e. D |-> ( A O B ) ) e. _V /\ Z e. _V ) -> ( ( x e. D |-> ( A O B ) ) supp Z ) = (/) )
45 43 44 sylnbi 
 |-  ( -. ( D e. _V /\ Z e. _V ) -> ( ( x e. D |-> ( A O B ) ) supp Z ) = (/) )
46 0ss 
 |-  (/) C_ L
47 45 46 eqsstrdi 
 |-  ( -. ( D e. _V /\ Z e. _V ) -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ L )
48 47 adantl 
 |-  ( ( ph /\ -. ( D e. _V /\ Z e. _V ) ) -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ L )
49 34 48 pm2.61dan 
 |-  ( ph -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ L )