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 ⊢φ→x∈D⟼BsuppY⊆L
suppssov2.o ⊢φ∧v∈R→vOY=Z
suppssov2.a ⊢φ∧x∈D→A∈R
suppssov2.b ⊢φ∧x∈D→B∈V
suppssov2.y ⊢φ→Y∈W
Assertion suppssov2 ⊢φ→x∈D⟼AOBsuppZ⊆L

Proof

Step Hyp Ref Expression
1 suppssov2.s ⊢φ→x∈D⟼BsuppY⊆L
2 suppssov2.o ⊢φ∧v∈R→vOY=Z
3 suppssov2.a ⊢φ∧x∈D→A∈R
4 suppssov2.b ⊢φ∧x∈D→B∈V
5 suppssov2.y ⊢φ→Y∈W
6 4 elexd ⊢φ∧x∈D→B∈V
7 6 adantlr ⊢φ∧D∈V∧Z∈V∧x∈D→B∈V
8 7 adantr ⊢φ∧D∈V∧Z∈V∧x∈D∧AOB∈V∖Z→B∈V
9 oveq1 ⊢v=A→vOY=AOY
10 9 eqeq1d ⊢v=A→vOY=Z↔AOY=Z
11 2 ralrimiva ⊢φ→∀v∈RvOY=Z
12 11 ad2antrr ⊢φ∧D∈V∧Z∈V∧x∈D→∀v∈RvOY=Z
13 3 adantlr ⊢φ∧D∈V∧Z∈V∧x∈D→A∈R
14 10 12 13 rspcdva ⊢φ∧D∈V∧Z∈V∧x∈D→AOY=Z
15 oveq2 ⊢B=Y→AOB=AOY
16 15 eqeq1d ⊢B=Y→AOB=Z↔AOY=Z
17 14 16 syl5ibrcom ⊢φ∧D∈V∧Z∈V∧x∈D→B=Y→AOB=Z
18 17 necon3d ⊢φ∧D∈V∧Z∈V∧x∈D→AOB≠Z→B≠Y
19 eldifsni ⊢AOB∈V∖Z→AOB≠Z
20 18 19 impel ⊢φ∧D∈V∧Z∈V∧x∈D∧AOB∈V∖Z→B≠Y
21 eldifsn ⊢B∈V∖Y↔B∈V∧B≠Y
22 8 20 21 sylanbrc ⊢φ∧D∈V∧Z∈V∧x∈D∧AOB∈V∖Z→B∈V∖Y
23 22 ex ⊢φ∧D∈V∧Z∈V∧x∈D→AOB∈V∖Z→B∈V∖Y
24 23 ss2rabdv ⊢φ∧D∈V∧Z∈V→x∈D|AOB∈V∖Z⊆x∈D|B∈V∖Y
25 eqid ⊢x∈D⟼AOB=x∈D⟼AOB
26 simprl ⊢φ∧D∈V∧Z∈V→D∈V
27 simprr ⊢φ∧D∈V∧Z∈V→Z∈V
28 25 26 27 mptsuppdifd ⊢φ∧D∈V∧Z∈V→x∈D⟼AOBsuppZ=x∈D|AOB∈V∖Z
29 eqid ⊢x∈D⟼B=x∈D⟼B
30 5 adantr ⊢φ∧D∈V∧Z∈V→Y∈W
31 29 26 30 mptsuppdifd ⊢φ∧D∈V∧Z∈V→x∈D⟼BsuppY=x∈D|B∈V∖Y
32 24 28 31 3sstr4d ⊢φ∧D∈V∧Z∈V→x∈D⟼AOBsuppZ⊆x∈D⟼BsuppY
33 1 adantr ⊢φ∧D∈V∧Z∈V→x∈D⟼BsuppY⊆L
34 32 33 sstrd ⊢φ∧D∈V∧Z∈V→x∈D⟼AOBsuppZ⊆L
35 mptexg ⊢D∈V→x∈D⟼AOB∈V
36 ovex ⊢AOB∈V
37 36 rgenw ⊢∀x∈DAOB∈V
38 dmmptg ⊢∀x∈DAOB∈V→dom⁡x∈D⟼AOB=D
39 37 38 ax-mp ⊢dom⁡x∈D⟼AOB=D
40 dmexg ⊢x∈D⟼AOB∈V→dom⁡x∈D⟼AOB∈V
41 39 40 eqeltrrid ⊢x∈D⟼AOB∈V→D∈V
42 35 41 impbii ⊢D∈V↔x∈D⟼AOB∈V
43 42 anbi1i ⊢D∈V∧Z∈V↔x∈D⟼AOB∈V∧Z∈V
44 supp0prc ⊢¬x∈D⟼AOB∈V∧Z∈V→x∈D⟼AOBsuppZ=∅
45 43 44 sylnbi ⊢¬D∈V∧Z∈V→x∈D⟼AOBsuppZ=∅
46 0ss ⊢∅⊆L
47 45 46 eqsstrdi ⊢¬D∈V∧Z∈V→x∈D⟼AOBsuppZ⊆L
48 47 adantl ⊢φ∧¬D∈V∧Z∈V→x∈D⟼AOBsuppZ⊆L
49 34 48 pm2.61dan ⊢φ→x∈D⟼AOBsuppZ⊆L