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