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 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) ⊆ 𝐿 )
suppssov1.o ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑅 ) → ( 𝑌 𝑂 𝑣 ) = 𝑍 )
suppssov1.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝑉 )
suppssov1.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐵 ∈ 𝑅 )
suppssov1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑊 )
Assertion suppssov1 ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 )

Proof

Step Hyp Ref Expression
1 suppssov1.s ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) ⊆ 𝐿 )
2 suppssov1.o ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑅 ) → ( 𝑌 𝑂 𝑣 ) = 𝑍 )
3 suppssov1.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝑉 )
4 suppssov1.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐵 ∈ 𝑅 )
5 suppssov1.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑊 )
6 3 elexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ V )
7 6 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ V )
8 7 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) ) → 𝐴 ∈ V )
9 oveq2 ⊢ ( 𝑣 = 𝐵 → ( 𝑌 𝑂 𝑣 ) = ( 𝑌 𝑂 𝐵 ) )
10 9 eqeq1d ⊢ ( 𝑣 = 𝐵 → ( ( 𝑌 𝑂 𝑣 ) = 𝑍 ↔ ( 𝑌 𝑂 𝐵 ) = 𝑍 ) )
11 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝑅 ( 𝑌 𝑂 𝑣 ) = 𝑍 )
12 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) → ∀ 𝑣 ∈ 𝑅 ( 𝑌 𝑂 𝑣 ) = 𝑍 )
13 4 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝐵 ∈ 𝑅 )
14 10 12 13 rspcdva ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝑌 𝑂 𝐵 ) = 𝑍 )
15 oveq1 ⊢ ( 𝐴 = 𝑌 → ( 𝐴 𝑂 𝐵 ) = ( 𝑌 𝑂 𝐵 ) )
16 15 eqeq1d ⊢ ( 𝐴 = 𝑌 → ( ( 𝐴 𝑂 𝐵 ) = 𝑍 ↔ ( 𝑌 𝑂 𝐵 ) = 𝑍 ) )
17 14 16 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 = 𝑌 → ( 𝐴 𝑂 𝐵 ) = 𝑍 ) )
18 17 necon3d ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐴 𝑂 𝐵 ) ≠ 𝑍 → 𝐴 ≠ 𝑌 ) )
19 eldifsni ⊢ ( ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) → ( 𝐴 𝑂 𝐵 ) ≠ 𝑍 )
20 18 19 impel ⊢ ( ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) ) → 𝐴 ≠ 𝑌 )
21 eldifsn ⊢ ( 𝐴 ∈ ( V ∖ { 𝑌 } ) ↔ ( 𝐴 ∈ V ∧ 𝐴 ≠ 𝑌 ) )
22 8 20 21 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) ) → 𝐴 ∈ ( V ∖ { 𝑌 } ) )
23 22 ex ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) → 𝐴 ∈ ( V ∖ { 𝑌 } ) ) )
24 23 ss2rabdv ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) } ⊆ { 𝑥 ∈ 𝐷 ∣ 𝐴 ∈ ( V ∖ { 𝑌 } ) } )
25 eqid ⊢ ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) )
26 simprl ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) → 𝐷 ∈ V )
27 simprr ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) → 𝑍 ∈ V )
28 25 26 27 mptsuppdifd ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) = { 𝑥 ∈ 𝐷 ∣ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) } )
29 eqid ⊢ ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) = ( 𝑥 ∈ 𝐷 ↦ 𝐴 )
30 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) → 𝑌 ∈ 𝑊 )
31 29 26 30 mptsuppdifd ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) = { 𝑥 ∈ 𝐷 ∣ 𝐴 ∈ ( V ∖ { 𝑌 } ) } )
32 24 28 31 3sstr4d ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) )
33 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) ⊆ 𝐿 )
34 32 33 sstrd ⊢ ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 )
35 mptexg ⊢ ( 𝐷 ∈ V → ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V )
36 ovex ⊢ ( 𝐴 𝑂 𝐵 ) ∈ V
37 36 rgenw ⊢ ∀ 𝑥 ∈ 𝐷 ( 𝐴 𝑂 𝐵 ) ∈ V
38 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝐷 ( 𝐴 𝑂 𝐵 ) ∈ V → dom ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) = 𝐷 )
39 37 38 ax-mp ⊢ dom ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) = 𝐷
40 dmexg ⊢ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V → dom ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V )
41 39 40 eqeltrrid ⊢ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V → 𝐷 ∈ V )
42 35 41 impbii ⊢ ( 𝐷 ∈ V ↔ ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V )
43 42 anbi1i ⊢ ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ↔ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V ∧ 𝑍 ∈ V ) )
44 supp0prc ⊢ ( ¬ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) = ∅ )
45 43 44 sylnbi ⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) = ∅ )
46 0ss ⊢ ∅ ⊆ 𝐿
47 45 46 eqsstrdi ⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 )
48 47 adantl ⊢ ( ( 𝜑 ∧ ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 )
49 34 48 pm2.61dan ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 )