This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 suppssov2.s ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) supp 𝑌 ) ⊆ 𝐿 )
2 suppssov2.o ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑅 ) → ( 𝑣 𝑂 𝑌 ) = 𝑍 )
3 suppssov2.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝑅 )
4 suppssov2.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐵 ∈ 𝑉 )
5 suppssov2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑊 )
6 4 elexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐵 ∈ V )
7 6 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝐵 ∈ V )
8 7 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝑂 𝐵 ) ∈ ( V ∖ { 𝑍 } ) ) → 𝐵 ∈ V )
9 oveq1 ⊢ ( 𝑣 = 𝐴 → ( 𝑣 𝑂 𝑌 ) = ( 𝐴 𝑂 𝑌 ) )
10 9 eqeq1d ⊢ ( 𝑣 = 𝐴 → ( ( 𝑣 𝑂 𝑌 ) = 𝑍 ↔ ( 𝐴 𝑂 𝑌 ) = 𝑍 ) )
11 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝑅 ( 𝑣 𝑂 𝑌 ) = 𝑍 )
12 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) → ∀ 𝑣 ∈ 𝑅 ( 𝑣 𝑂 𝑌 ) = 𝑍 )
13 3 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝑅 )
14 10 12 13 rspcdva ⊢ ( ( ( 𝜑 ∧ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ) ∧ 𝑥 ∈ 𝐷 ) → ( 𝐴 𝑂 𝑌 ) = 𝑍 )
15 oveq2 ⊢ ( 𝐵 = 𝑌 → ( 𝐴 𝑂 𝐵 ) = ( 𝐴 𝑂 𝑌 ) )
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 𝑍 ) ⊆ 𝐿 )