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

Proof

Step Hyp Ref Expression
1 suppssov2.s ⊢ φ → x ∈ D ⟼ B supp Y ⊆ L
2 suppssov2.o ⊢ φ ∧ v ∈ R → v O Y = 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 ∧ A O B ∈ V ∖ Z → B ∈ 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 ⊢ φ → ∀ v ∈ R v O Y = Z
12 11 ad2antrr ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D → ∀ v ∈ R v O Y = Z
13 3 adantlr ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D → A ∈ R
14 10 12 13 rspcdva ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ 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 ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D → B = Y → A O B = Z
18 17 necon3d ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D → A O B ≠ Z → B ≠ Y
19 eldifsni ⊢ A O B ∈ V ∖ Z → A O B ≠ Z
20 18 19 impel ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D ∧ A O B ∈ V ∖ Z → B ≠ Y
21 eldifsn ⊢ B ∈ V ∖ Y ↔ B ∈ V ∧ B ≠ Y
22 8 20 21 sylanbrc ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D ∧ A O B ∈ V ∖ Z → B ∈ V ∖ Y
23 22 ex ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D → A O B ∈ V ∖ Z → B ∈ V ∖ Y
24 23 ss2rabdv ⊢ φ ∧ D ∈ V ∧ Z ∈ V → x ∈ D | A O B ∈ V ∖ Z ⊆ x ∈ D | B ∈ V ∖ Y
25 eqid ⊢ x ∈ D ⟼ A O B = x ∈ D ⟼ A O B
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 ⟼ A O B supp Z = x ∈ D | A O B ∈ 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 ⟼ B supp Y = x ∈ D | B ∈ V ∖ Y
32 24 28 31 3sstr4d ⊢ φ ∧ D ∈ V ∧ Z ∈ V → x ∈ D ⟼ A O B supp Z ⊆ x ∈ D ⟼ B supp Y
33 1 adantr ⊢ φ ∧ D ∈ V ∧ Z ∈ V → x ∈ D ⟼ B supp Y ⊆ L
34 32 33 sstrd ⊢ φ ∧ D ∈ V ∧ Z ∈ V → x ∈ D ⟼ A O B supp Z ⊆ L
35 mptexg ⊢ D ∈ V → x ∈ D ⟼ A O B ∈ V
36 ovex ⊢ A O B ∈ V
37 36 rgenw ⊢ ∀ x ∈ D A O B ∈ V
38 dmmptg ⊢ ∀ x ∈ D A O B ∈ V → dom ⁡ x ∈ D ⟼ A O B = D
39 37 38 ax-mp ⊢ dom ⁡ x ∈ D ⟼ A O B = D
40 dmexg ⊢ x ∈ D ⟼ A O B ∈ V → dom ⁡ x ∈ D ⟼ A O B ∈ V
41 39 40 eqeltrrid ⊢ x ∈ D ⟼ A O B ∈ V → D ∈ V
42 35 41 impbii ⊢ D ∈ V ↔ x ∈ D ⟼ A O B ∈ V
43 42 anbi1i ⊢ D ∈ V ∧ Z ∈ V ↔ x ∈ D ⟼ A O B ∈ V ∧ Z ∈ V
44 supp0prc ⊢ ¬ x ∈ D ⟼ A O B ∈ V ∧ Z ∈ V → x ∈ D ⟼ A O B supp Z = ∅
45 43 44 sylnbi ⊢ ¬ D ∈ V ∧ Z ∈ V → x ∈ D ⟼ A O B supp Z = ∅
46 0ss ⊢ ∅ ⊆ L
47 45 46 eqsstrdi ⊢ ¬ D ∈ V ∧ Z ∈ V → x ∈ D ⟼ A O B supp Z ⊆ L
48 47 adantl ⊢ φ ∧ ¬ D ∈ V ∧ Z ∈ V → x ∈ D ⟼ A O B supp Z ⊆ L
49 34 48 pm2.61dan ⊢ φ → x ∈ D ⟼ A O B supp Z ⊆ L