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

Proof

Step Hyp Ref Expression
1 suppssov1.s ⊢ φ → x ∈ D ⟼ A supp Y ⊆ L
2 suppssov1.o ⊢ φ ∧ v ∈ R → Y O v = Z
3 suppssov1.a ⊢ φ ∧ x ∈ D → A ∈ V
4 suppssov1.b ⊢ φ ∧ x ∈ D → B ∈ R
5 suppssov1.y ⊢ φ → Y ∈ W
6 3 elexd ⊢ φ ∧ x ∈ D → A ∈ V
7 6 adantlr ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D → A ∈ V
8 7 adantr ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D ∧ A O B ∈ V ∖ Z → A ∈ 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 ⊢ φ → ∀ v ∈ R Y O v = Z
12 11 ad2antrr ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D → ∀ v ∈ R Y O v = Z
13 4 adantlr ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D → B ∈ R
14 10 12 13 rspcdva ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ 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 ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D → A = Y → A O B = Z
18 17 necon3d ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D → A O B ≠ Z → A ≠ 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 → A ≠ Y
21 eldifsn ⊢ A ∈ V ∖ Y ↔ A ∈ V ∧ A ≠ Y
22 8 20 21 sylanbrc ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D ∧ A O B ∈ V ∖ Z → A ∈ V ∖ Y
23 22 ex ⊢ φ ∧ D ∈ V ∧ Z ∈ V ∧ x ∈ D → A O B ∈ V ∖ Z → A ∈ V ∖ Y
24 23 ss2rabdv ⊢ φ ∧ D ∈ V ∧ Z ∈ V → x ∈ D | A O B ∈ V ∖ Z ⊆ x ∈ D | A ∈ 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 ⟼ A = x ∈ D ⟼ A
30 5 adantr ⊢ φ ∧ D ∈ V ∧ Z ∈ V → Y ∈ W
31 29 26 30 mptsuppdifd ⊢ φ ∧ D ∈ V ∧ Z ∈ V → x ∈ D ⟼ A supp Y = x ∈ D | A ∈ V ∖ Y
32 24 28 31 3sstr4d ⊢ φ ∧ D ∈ V ∧ Z ∈ V → x ∈ D ⟼ A O B supp Z ⊆ x ∈ D ⟼ A supp Y
33 1 adantr ⊢ φ ∧ D ∈ V ∧ Z ∈ V → x ∈ D ⟼ A 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