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 𝑍 ) ⊆ 𝐿 )