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 ( 𝜑 → ( ( 𝑥𝐷𝐴 ) 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 adantll ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥𝐷 ) → 𝐴 ∈ V )
8 7 adantr ( ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥𝐷 ) ∧ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) ) → 𝐴 ∈ V )
9 oveq2 ( 𝑣 = 𝐵 → ( 𝑌 𝑂 𝑣 ) = ( 𝑌 𝑂 𝐵 ) )
10 9 eqeq1d ( 𝑣 = 𝐵 → ( ( 𝑌 𝑂 𝑣 ) = 𝑍 ↔ ( 𝑌 𝑂 𝐵 ) = 𝑍 ) )
11 2 ralrimiva ( 𝜑 → ∀ 𝑣𝑅 ( 𝑌 𝑂 𝑣 ) = 𝑍 )
12 11 adantl ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ∀ 𝑣𝑅 ( 𝑌 𝑂 𝑣 ) = 𝑍 )
13 12 adantr ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥𝐷 ) → ∀ 𝑣𝑅 ( 𝑌 𝑂 𝑣 ) = 𝑍 )
14 4 adantll ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥𝐷 ) → 𝐵𝑅 )
15 10 13 14 rspcdva ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥𝐷 ) → ( 𝑌 𝑂 𝐵 ) = 𝑍 )
16 oveq1 ( 𝐴 = 𝑌 → ( 𝐴 𝑂 𝐵 ) = ( 𝑌 𝑂 𝐵 ) )
17 16 eqeq1d ( 𝐴 = 𝑌 → ( ( 𝐴 𝑂 𝐵 ) = 𝑍 ↔ ( 𝑌 𝑂 𝐵 ) = 𝑍 ) )
18 15 17 syl5ibrcom ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥𝐷 ) → ( 𝐴 = 𝑌 → ( 𝐴 𝑂 𝐵 ) = 𝑍 ) )
19 18 necon3d ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥𝐷 ) → ( ( 𝐴 𝑂 𝐵 ) ≠ 𝑍𝐴𝑌 ) )
20 eldifsni ( ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) → ( 𝐴 𝑂 𝐵 ) ≠ 𝑍 )
21 19 20 impel ( ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥𝐷 ) ∧ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) ) → 𝐴𝑌 )
22 eldifsn ( 𝐴 ∈ ( V ∖ { 𝑌 } ) ↔ ( 𝐴 ∈ V ∧ 𝐴𝑌 ) )
23 8 21 22 sylanbrc ( ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥𝐷 ) ∧ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) ) → 𝐴 ∈ ( V ∖ { 𝑌 } ) )
24 23 ex ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥𝐷 ) → ( ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) → 𝐴 ∈ ( V ∖ { 𝑌 } ) ) )
25 24 ss2rabdv ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → { 𝑥𝐷 ∣ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) } ⊆ { 𝑥𝐷𝐴 ∈ ( V ∖ { 𝑌 } ) } )
26 eqid ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) = ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) )
27 simpll ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝐷 ∈ V )
28 simplr ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝑍 ∈ V )
29 26 27 28 mptsuppdifd ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) = { 𝑥𝐷 ∣ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) } )
30 eqid ( 𝑥𝐷𝐴 ) = ( 𝑥𝐷𝐴 )
31 5 adantl ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝑌𝑊 )
32 30 27 31 mptsuppdifd ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥𝐷𝐴 ) supp 𝑌 ) = { 𝑥𝐷𝐴 ∈ ( V ∖ { 𝑌 } ) } )
33 25 29 32 3sstr4d ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ ( ( 𝑥𝐷𝐴 ) supp 𝑌 ) )
34 1 adantl ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥𝐷𝐴 ) supp 𝑌 ) ⊆ 𝐿 )
35 33 34 sstrd ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 )
36 35 ex ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 ) )
37 mptexg ( 𝐷 ∈ V → ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V )
38 ovex ( 𝐴 𝑂 𝐵 ) ∈ V
39 38 rgenw 𝑥𝐷 ( 𝐴 𝑂 𝐵 ) ∈ V
40 dmmptg ( ∀ 𝑥𝐷 ( 𝐴 𝑂 𝐵 ) ∈ V → dom ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) = 𝐷 )
41 39 40 ax-mp dom ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) = 𝐷
42 dmexg ( ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V → dom ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V )
43 41 42 eqeltrrid ( ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V → 𝐷 ∈ V )
44 37 43 impbii ( 𝐷 ∈ V ↔ ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V )
45 44 anbi1i ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ↔ ( ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V ∧ 𝑍 ∈ V ) )
46 supp0prc ( ¬ ( ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) = ∅ )
47 45 46 sylnbi ( ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) = ∅ )
48 0ss ∅ ⊆ 𝐿
49 47 48 eqsstrdi ( ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 )
50 49 a1d ( ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 ) )
51 36 50 pm2.61i ( 𝜑 → ( ( 𝑥𝐷 ↦ ( 𝐴 𝑂 𝐵 ) ) supp 𝑍 ) ⊆ 𝐿 )