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 ⊢ φ → 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 adantll ⊢ 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 adantl ⊢ D ∈ V ∧ Z ∈ V ∧ φ → ∀ v ∈ R Y O v = Z
13 12 adantr ⊢ D ∈ V ∧ Z ∈ V ∧ φ ∧ x ∈ D → ∀ v ∈ R Y O v = Z
14 4 adantll ⊢ D ∈ V ∧ Z ∈ V ∧ φ ∧ x ∈ D → B ∈ R
15 10 13 14 rspcdva ⊢ D ∈ V ∧ Z ∈ V ∧ φ ∧ x ∈ 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 ∈ V ∧ Z ∈ V ∧ φ ∧ x ∈ D → A = Y → A O B = Z
19 18 necon3d ⊢ D ∈ V ∧ Z ∈ V ∧ φ ∧ x ∈ D → A O B ≠ Z → A ≠ Y
20 eldifsni ⊢ A O B ∈ V ∖ Z → A O B ≠ Z
21 19 20 impel ⊢ D ∈ V ∧ Z ∈ V ∧ φ ∧ x ∈ D ∧ A O B ∈ V ∖ Z → A ≠ Y
22 eldifsn ⊢ A ∈ V ∖ Y ↔ A ∈ V ∧ A ≠ Y
23 8 21 22 sylanbrc ⊢ D ∈ V ∧ Z ∈ V ∧ φ ∧ x ∈ D ∧ A O B ∈ V ∖ Z → A ∈ V ∖ Y
24 23 ex ⊢ D ∈ V ∧ Z ∈ V ∧ φ ∧ x ∈ D → A O B ∈ V ∖ Z → A ∈ V ∖ Y
25 24 ss2rabdv ⊢ D ∈ V ∧ Z ∈ V ∧ φ → x ∈ D | A O B ∈ V ∖ Z ⊆ x ∈ D | A ∈ V ∖ Y
26 eqid ⊢ x ∈ D ⟼ A O B = x ∈ D ⟼ A O B
27 simpll ⊢ D ∈ V ∧ Z ∈ V ∧ φ → D ∈ V
28 simplr ⊢ D ∈ V ∧ Z ∈ V ∧ φ → Z ∈ V
29 26 27 28 mptsuppdifd ⊢ D ∈ V ∧ Z ∈ V ∧ φ → x ∈ D ⟼ A O B supp Z = x ∈ D | A O B ∈ V ∖ Z
30 eqid ⊢ x ∈ D ⟼ A = x ∈ D ⟼ A
31 5 adantl ⊢ D ∈ V ∧ Z ∈ V ∧ φ → Y ∈ W
32 30 27 31 mptsuppdifd ⊢ D ∈ V ∧ Z ∈ V ∧ φ → x ∈ D ⟼ A supp Y = x ∈ D | A ∈ V ∖ Y
33 25 29 32 3sstr4d ⊢ D ∈ V ∧ Z ∈ V ∧ φ → x ∈ D ⟼ A O B supp Z ⊆ x ∈ D ⟼ A supp Y
34 1 adantl ⊢ D ∈ V ∧ Z ∈ V ∧ φ → x ∈ D ⟼ A supp Y ⊆ L
35 33 34 sstrd ⊢ D ∈ V ∧ Z ∈ V ∧ φ → x ∈ D ⟼ A O B supp Z ⊆ L
36 35 ex ⊢ D ∈ V ∧ Z ∈ V → φ → x ∈ D ⟼ A O B supp Z ⊆ L
37 mptexg ⊢ D ∈ V → x ∈ D ⟼ A O B ∈ V
38 ovex ⊢ A O B ∈ V
39 38 rgenw ⊢ ∀ x ∈ D A O B ∈ V
40 dmmptg ⊢ ∀ x ∈ D A O B ∈ V → dom ⁡ x ∈ D ⟼ A O B = D
41 39 40 ax-mp ⊢ dom ⁡ x ∈ D ⟼ A O B = D
42 dmexg ⊢ x ∈ D ⟼ A O B ∈ V → dom ⁡ x ∈ D ⟼ A O B ∈ V
43 41 42 eqeltrrid ⊢ x ∈ D ⟼ A O B ∈ V → D ∈ V
44 37 43 impbii ⊢ D ∈ V ↔ x ∈ D ⟼ A O B ∈ V
45 44 anbi1i ⊢ D ∈ V ∧ Z ∈ V ↔ x ∈ D ⟼ A O B ∈ V ∧ Z ∈ V
46 supp0prc ⊢ ¬ x ∈ D ⟼ A O B ∈ V ∧ Z ∈ V → x ∈ D ⟼ A O B supp Z = ∅
47 45 46 sylnbi ⊢ ¬ D ∈ V ∧ Z ∈ V → x ∈ D ⟼ A O B supp Z = ∅
48 0ss ⊢ ∅ ⊆ L
49 47 48 eqsstrdi ⊢ ¬ D ∈ V ∧ Z ∈ V → x ∈ D ⟼ A O B supp Z ⊆ L
50 49 a1d ⊢ ¬ D ∈ V ∧ Z ∈ V → φ → x ∈ D ⟼ A O B supp Z ⊆ L
51 36 50 pm2.61i ⊢ φ → x ∈ D ⟼ A O B supp Z ⊆ L