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)

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 adantll 
 |-  ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) -> A e. _V )
8 7 adantr 
 |-  ( ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ 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 adantl 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> A. v e. R ( Y O v ) = Z )
13 12 adantr 
 |-  ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) -> A. v e. R ( Y O v ) = Z )
14 4 adantll 
 |-  ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) -> B e. R )
15 10 13 14 rspcdva 
 |-  ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) -> ( Y O B ) = Z )
16 oveq1 
 |-  ( A = Y -> ( A O B ) = ( Y O B ) )
17 16 eqeq1d 
 |-  ( A = Y -> ( ( A O B ) = Z <-> ( Y O B ) = Z ) )
18 15 17 syl5ibrcom 
 |-  ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) -> ( A = Y -> ( A O B ) = Z ) )
19 18 necon3d 
 |-  ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) -> ( ( A O B ) =/= Z -> A =/= Y ) )
20 eldifsni 
 |-  ( ( A O B ) e. ( _V \ { Z } ) -> ( A O B ) =/= Z )
21 19 20 impel 
 |-  ( ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) /\ ( A O B ) e. ( _V \ { Z } ) ) -> A =/= Y )
22 eldifsn 
 |-  ( A e. ( _V \ { Y } ) <-> ( A e. _V /\ A =/= Y ) )
23 8 21 22 sylanbrc 
 |-  ( ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) /\ ( A O B ) e. ( _V \ { Z } ) ) -> A e. ( _V \ { Y } ) )
24 23 ex 
 |-  ( ( ( ( D e. _V /\ Z e. _V ) /\ ph ) /\ x e. D ) -> ( ( A O B ) e. ( _V \ { Z } ) -> A e. ( _V \ { Y } ) ) )
25 24 ss2rabdv 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> { x e. D | ( A O B ) e. ( _V \ { Z } ) } C_ { x e. D | A e. ( _V \ { Y } ) } )
26 eqid 
 |-  ( x e. D |-> ( A O B ) ) = ( x e. D |-> ( A O B ) )
27 simpll 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> D e. _V )
28 simplr 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> Z e. _V )
29 26 27 28 mptsuppdifd 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> ( ( x e. D |-> ( A O B ) ) supp Z ) = { x e. D | ( A O B ) e. ( _V \ { Z } ) } )
30 eqid 
 |-  ( x e. D |-> A ) = ( x e. D |-> A )
31 5 adantl 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> Y e. W )
32 30 27 31 mptsuppdifd 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> ( ( x e. D |-> A ) supp Y ) = { x e. D | A e. ( _V \ { Y } ) } )
33 25 29 32 3sstr4d 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ ( ( x e. D |-> A ) supp Y ) )
34 1 adantl 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> ( ( x e. D |-> A ) supp Y ) C_ L )
35 33 34 sstrd 
 |-  ( ( ( D e. _V /\ Z e. _V ) /\ ph ) -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ L )
36 35 ex 
 |-  ( ( D e. _V /\ Z e. _V ) -> ( ph -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ L ) )
37 mptexg 
 |-  ( D e. _V -> ( x e. D |-> ( A O B ) ) e. _V )
38 ovex 
 |-  ( A O B ) e. _V
39 38 rgenw 
 |-  A. x e. D ( A O B ) e. _V
40 dmmptg 
 |-  ( A. x e. D ( A O B ) e. _V -> dom ( x e. D |-> ( A O B ) ) = D )
41 39 40 ax-mp 
 |-  dom ( x e. D |-> ( A O B ) ) = D
42 dmexg 
 |-  ( ( x e. D |-> ( A O B ) ) e. _V -> dom ( x e. D |-> ( A O B ) ) e. _V )
43 41 42 eqeltrrid 
 |-  ( ( x e. D |-> ( A O B ) ) e. _V -> D e. _V )
44 37 43 impbii 
 |-  ( D e. _V <-> ( x e. D |-> ( A O B ) ) e. _V )
45 44 anbi1i 
 |-  ( ( D e. _V /\ Z e. _V ) <-> ( ( x e. D |-> ( A O B ) ) e. _V /\ Z e. _V ) )
46 supp0prc 
 |-  ( -. ( ( x e. D |-> ( A O B ) ) e. _V /\ Z e. _V ) -> ( ( x e. D |-> ( A O B ) ) supp Z ) = (/) )
47 45 46 sylnbi 
 |-  ( -. ( D e. _V /\ Z e. _V ) -> ( ( x e. D |-> ( A O B ) ) supp Z ) = (/) )
48 0ss 
 |-  (/) C_ L
49 47 48 eqsstrdi 
 |-  ( -. ( D e. _V /\ Z e. _V ) -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ L )
50 49 a1d 
 |-  ( -. ( D e. _V /\ Z e. _V ) -> ( ph -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ L ) )
51 36 50 pm2.61i 
 |-  ( ph -> ( ( x e. D |-> ( A O B ) ) supp Z ) C_ L )