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	$⊢ φ \to (x \in D ⟼ A) supp Y \subseteq L$
	suppssov1.o	$⊢ (φ \land v \in R) \to Y O v = Z$
	suppssov1.a	$⊢ (φ \land x \in D) \to A \in V$
	suppssov1.b	$⊢ (φ \land x \in D) \to B \in R$
	suppssov1.y	$⊢ φ \to Y \in W$
Assertion	suppssov1	$⊢ φ \to (x \in D ⟼ A O B) supp Z \subseteq L$

Proof

Step	Hyp	Ref	Expression
1		suppssov1.s	$⊢ φ \to (x \in D ⟼ A) supp Y \subseteq L$
2		suppssov1.o	$⊢ (φ \land v \in R) \to Y O v = Z$
3		suppssov1.a	$⊢ (φ \land x \in D) \to A \in V$
4		suppssov1.b	$⊢ (φ \land x \in D) \to B \in R$
5		suppssov1.y	$⊢ φ \to Y \in W$
6	3	elexd	$⊢ (φ \land x \in D) \to A \in V$
7	6	adantll	$⊢ (((D \in V \land Z \in V) \land φ) \land x \in D) \to A \in V$
8	7	adantr	$⊢ ((((D \in V \land Z \in V) \land φ) \land x \in D) \land A O B \in (V ∖ \{Z\})) \to A \in V$
9		oveq2	$⊢ v = B \to Y O v = Y O B$
10	9	eqeq1d	$⊢ v = B \to (Y O v = Z \leftrightarrow Y O B = Z)$
11	2	ralrimiva	$⊢ φ \to \forall v \in R Y O v = Z$
12	11	adantl	$⊢ ((D \in V \land Z \in V) \land φ) \to \forall v \in R Y O v = Z$
13	12	adantr	$⊢ (((D \in V \land Z \in V) \land φ) \land x \in D) \to \forall v \in R Y O v = Z$
14	4	adantll	$⊢ (((D \in V \land Z \in V) \land φ) \land x \in D) \to B \in R$
15	10 13 14	rspcdva	$⊢ (((D \in V \land Z \in V) \land φ) \land x \in D) \to Y O B = Z$
16		oveq1	$⊢ A = Y \to A O B = Y O B$
17	16	eqeq1d	$⊢ A = Y \to (A O B = Z \leftrightarrow Y O B = Z)$
18	15 17	syl5ibrcom	$⊢ (((D \in V \land Z \in V) \land φ) \land x \in D) \to (A = Y \to A O B = Z)$
19	18	necon3d	$⊢ (((D \in V \land Z \in V) \land φ) \land x \in D) \to (A O B \neq Z \to A \neq Y)$
20		eldifsni	$⊢ A O B \in (V ∖ \{Z\}) \to A O B \neq Z$
21	19 20	impel	$⊢ ((((D \in V \land Z \in V) \land φ) \land x \in D) \land A O B \in (V ∖ \{Z\})) \to A \neq Y$
22		eldifsn	$⊢ A \in (V ∖ \{Y\}) \leftrightarrow (A \in V \land A \neq Y)$
23	8 21 22	sylanbrc	$⊢ ((((D \in V \land Z \in V) \land φ) \land x \in D) \land A O B \in (V ∖ \{Z\})) \to A \in (V ∖ \{Y\})$
24	23	ex	$⊢ (((D \in V \land Z \in V) \land φ) \land x \in D) \to (A O B \in (V ∖ \{Z\}) \to A \in (V ∖ \{Y\}))$
25	24	ss2rabdv	$⊢ ((D \in V \land Z \in V) \land φ) \to \{x \in D \| A O B \in (V ∖ \{Z\})\} \subseteq \{x \in D \| A \in (V ∖ \{Y\})\}$
26		eqid	$⊢ (x \in D ⟼ A O B) = (x \in D ⟼ A O B)$
27		simpll	$⊢ ((D \in V \land Z \in V) \land φ) \to D \in V$
28		simplr	$⊢ ((D \in V \land Z \in V) \land φ) \to Z \in V$
29	26 27 28	mptsuppdifd	$⊢ ((D \in V \land Z \in V) \land φ) \to (x \in D ⟼ A O B) supp Z = \{x \in D \| A O B \in (V ∖ \{Z\})\}$
30		eqid	$⊢ (x \in D ⟼ A) = (x \in D ⟼ A)$
31	5	adantl	$⊢ ((D \in V \land Z \in V) \land φ) \to Y \in W$
32	30 27 31	mptsuppdifd	$⊢ ((D \in V \land Z \in V) \land φ) \to (x \in D ⟼ A) supp Y = \{x \in D \| A \in (V ∖ \{Y\})\}$
33	25 29 32	3sstr4d	$⊢ ((D \in V \land Z \in V) \land φ) \to (x \in D ⟼ A O B) supp Z \subseteq (x \in D ⟼ A) supp Y$
34	1	adantl	$⊢ ((D \in V \land Z \in V) \land φ) \to (x \in D ⟼ A) supp Y \subseteq L$
35	33 34	sstrd	$⊢ ((D \in V \land Z \in V) \land φ) \to (x \in D ⟼ A O B) supp Z \subseteq L$
36	35	ex	$⊢ (D \in V \land Z \in V) \to (φ \to (x \in D ⟼ A O B) supp Z \subseteq L)$
37		mptexg	$⊢ D \in V \to (x \in D ⟼ A O B) \in V$
38		ovex	$⊢ A O B \in V$
39	38	rgenw	$⊢ \forall x \in D A O B \in V$
40		dmmptg	$⊢ \forall x \in D A O B \in V \to dom (x \in D ⟼ A O B) = D$
41	39 40	ax-mp	$⊢ dom (x \in D ⟼ A O B) = D$
42		dmexg	$⊢ (x \in D ⟼ A O B) \in V \to dom (x \in D ⟼ A O B) \in V$
43	41 42	eqeltrrid	$⊢ (x \in D ⟼ A O B) \in V \to D \in V$
44	37 43	impbii	$⊢ D \in V \leftrightarrow (x \in D ⟼ A O B) \in V$
45	44	anbi1i	$⊢ (D \in V \land Z \in V) \leftrightarrow ((x \in D ⟼ A O B) \in V \land Z \in V)$
46		supp0prc	$⊢ \neg ((x \in D ⟼ A O B) \in V \land Z \in V) \to (x \in D ⟼ A O B) supp Z = \emptyset$
47	45 46	sylnbi	$⊢ \neg (D \in V \land Z \in V) \to (x \in D ⟼ A O B) supp Z = \emptyset$
48		0ss	$⊢ \emptyset \subseteq L$
49	47 48	eqsstrdi	$⊢ \neg (D \in V \land Z \in V) \to (x \in D ⟼ A O B) supp Z \subseteq L$
50	49	a1d	$⊢ \neg (D \in V \land Z \in V) \to (φ \to (x \in D ⟼ A O B) supp Z \subseteq L)$
51	36 50	pm2.61i	$⊢ φ \to (x \in D ⟼ A O B) supp Z \subseteq L$

Metamath Proof Explorer

Theorem suppssov1

Proof