Metamath Proof Explorer

Theorem 2mpo0

Description: If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. (Contributed by AV, 21-May-2021)

		Ref	Expression
	Hypotheses	2mpo0.o	$⊢ O = (x \in A, y \in B ⟼ E)$
		2mpo0.u	$⊢ (X \in A \land Y \in B) \to X O Y = (s \in C, t \in D ⟼ F)$
	Assertion	2mpo0	$⊢ \neg ((X \in A \land Y \in B) \land (S \in C \land T \in D)) \to S (X O Y) T = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		2mpo0.o	$⊢ O = (x \in A, y \in B ⟼ E)$
2		2mpo0.u	$⊢ (X \in A \land Y \in B) \to X O Y = (s \in C, t \in D ⟼ F)$
3		ianor	$⊢ \neg ((X \in A \land Y \in B) \land (S \in C \land T \in D)) \leftrightarrow (\neg (X \in A \land Y \in B) \lor \neg (S \in C \land T \in D))$
4	1	mpondm0	$⊢ \neg (X \in A \land Y \in B) \to X O Y = \emptyset$
5	4	oveqd	$⊢ \neg (X \in A \land Y \in B) \to S (X O Y) T = S \emptyset T$
6		0ov	$⊢ S \emptyset T = \emptyset$
7	5 6	eqtrdi	$⊢ \neg (X \in A \land Y \in B) \to S (X O Y) T = \emptyset$
8		notnotb	$⊢ (X \in A \land Y \in B) \leftrightarrow \neg \neg (X \in A \land Y \in B)$
9	2	adantr	$⊢ ((X \in A \land Y \in B) \land \neg (S \in C \land T \in D)) \to X O Y = (s \in C, t \in D ⟼ F)$
10	9	oveqd	$⊢ ((X \in A \land Y \in B) \land \neg (S \in C \land T \in D)) \to S (X O Y) T = S (s \in C, t \in D ⟼ F) T$
11		eqid	$⊢ (s \in C, t \in D ⟼ F) = (s \in C, t \in D ⟼ F)$
12	11	mpondm0	$⊢ \neg (S \in C \land T \in D) \to S (s \in C, t \in D ⟼ F) T = \emptyset$
13	12	adantl	$⊢ ((X \in A \land Y \in B) \land \neg (S \in C \land T \in D)) \to S (s \in C, t \in D ⟼ F) T = \emptyset$
14	10 13	eqtrd	$⊢ ((X \in A \land Y \in B) \land \neg (S \in C \land T \in D)) \to S (X O Y) T = \emptyset$
15	8 14	sylanbr	$⊢ (\neg \neg (X \in A \land Y \in B) \land \neg (S \in C \land T \in D)) \to S (X O Y) T = \emptyset$
16	7 15	jaoi3	$⊢ (\neg (X \in A \land Y \in B) \lor \neg (S \in C \land T \in D)) \to S (X O Y) T = \emptyset$
17	3 16	sylbi	$⊢ \neg ((X \in A \land Y \in B) \land (S \in C \land T \in D)) \to S (X O Y) T = \emptyset$