Metamath Proof Explorer

Theorem suppssov2

Description: Formula building theorem for support restrictions: operator with right annihilator. (Contributed by SN, 11-Apr-2025)

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

Proof

Step Hyp Ref Expression
1 suppssov2.s 
 |-  ( ph -> ( ( x e. D |-> B ) supp Y ) C_ L )
2 suppssov2.o 
 |-  ( ( ph /\ v e. R ) -> ( v O Y ) = Z )
3 suppssov2.a 
 |-  ( ( ph /\ x e. D ) -> A e. R )
4 suppssov2.b 
 |-  ( ( ph /\ x e. D ) -> B e. V )
5 suppssov2.y 
 |-  ( ph -> Y e. W )
6 4 elexd 
 |-  ( ( ph /\ x e. D ) -> B e. _V )
7 6 adantlr 
 |-  ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) -> B e. _V )
8 7 adantr 
 |-  ( ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) /\ ( A O B ) e. ( _V \ { Z } ) ) -> B e. _V )
9 oveq1 
 |-  ( v = A -> ( v O Y ) = ( A O Y ) )
10 9 eqeq1d 
 |-  ( v = A -> ( ( v O Y ) = Z <-> ( A O Y ) = Z ) )
11 2 ralrimiva 
 |-  ( ph -> A. v e. R ( v O Y ) = Z )
12 11 ad2antrr 
 |-  ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) -> A. v e. R ( v O Y ) = Z )
13 3 adantlr 
 |-  ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) -> A e. R )
14 10 12 13 rspcdva 
 |-  ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) -> ( A O Y ) = Z )
15 oveq2 
 |-  ( B = Y -> ( A O B ) = ( A O Y ) )
16 15 eqeq1d 
 |-  ( B = Y -> ( ( A O B ) = Z <-> ( A O Y ) = Z ) )
17 14 16 syl5ibrcom 
 |-  ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) -> ( B = Y -> ( A O B ) = Z ) )
18 17 necon3d 
 |-  ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) -> ( ( A O B ) =/= Z -> B =/= 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 } ) ) -> B =/= Y )
21 eldifsn 
 |-  ( B e. ( _V \ { Y } ) <-> ( B e. _V /\ B =/= Y ) )
22 8 20 21 sylanbrc 
 |-  ( ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) /\ ( A O B ) e. ( _V \ { Z } ) ) -> B e. ( _V \ { Y } ) )
23 22 ex 
 |-  ( ( ( ph /\ ( D e. _V /\ Z e. _V ) ) /\ x e. D ) -> ( ( A O B ) e. ( _V \ { Z } ) -> B 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 | B 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 |-> B ) = ( x e. D |-> B )
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 |-> B ) supp Y ) = { x e. D | B 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 |-> B ) supp Y ) )
33 1 adantr 
 |-  ( ( ph /\ ( D e. _V /\ Z e. _V ) ) -> ( ( x e. D |-> B ) 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 )