el2mpocl

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. Using implicit substitution. (Contributed by AV, 21-May-2021)

	Ref	Expression
Hypotheses	el2mpocl.o	$⊢ O = (x \in A, y \in B ⟼ (s \in C, t \in D ⟼ E))$
	el2mpocl.e	$⊢ (x = X \land y = Y) \to (C = F \land D = G)$
Assertion	el2mpocl	$⊢ \forall x \in A \forall y \in B (C \in U \land D \in V) \to (W \in (S (X O Y) T) \to ((X \in A \land Y \in B) \land (S \in F \land T \in G)))$

Proof

Step	Hyp	Ref	Expression
1		el2mpocl.o	$⊢ O = (x \in A, y \in B ⟼ (s \in C, t \in D ⟼ E))$
2		el2mpocl.e	$⊢ (x = X \land y = Y) \to (C = F \land D = G)$
3	1	el2mpocsbcl	$⊢ \forall x \in A \forall y \in B (C \in U \land D \in V) \to (W \in (S (X O Y) T) \to ((X \in A \land Y \in B) \land (S \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C \land T \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D)))$
4		simpl	$⊢ (X \in A \land Y \in B) \to X \in A$
5		simplr	$⊢ ((X \in A \land Y \in B) \land x = X) \to Y \in B$
6	2	simpld	$⊢ (x = X \land y = Y) \to C = F$
7	6	adantll	$⊢ (((X \in A \land Y \in B) \land x = X) \land y = Y) \to C = F$
8	5 7	csbied	$⊢ ((X \in A \land Y \in B) \land x = X) \to ⦋ Y / y ⦌ C = F$
9	4 8	csbied	$⊢ (X \in A \land Y \in B) \to ⦋ X / x ⦌ ⦋ Y / y ⦌ C = F$
10	9	eleq2d	$⊢ (X \in A \land Y \in B) \to (S \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C \leftrightarrow S \in F)$
11	2	simprd	$⊢ (x = X \land y = Y) \to D = G$
12	11	adantll	$⊢ (((X \in A \land Y \in B) \land x = X) \land y = Y) \to D = G$
13	5 12	csbied	$⊢ ((X \in A \land Y \in B) \land x = X) \to ⦋ Y / y ⦌ D = G$
14	4 13	csbied	$⊢ (X \in A \land Y \in B) \to ⦋ X / x ⦌ ⦋ Y / y ⦌ D = G$
15	14	eleq2d	$⊢ (X \in A \land Y \in B) \to (T \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D \leftrightarrow T \in G)$
16	10 15	anbi12d	$⊢ (X \in A \land Y \in B) \to ((S \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C \land T \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D) \leftrightarrow (S \in F \land T \in G))$
17	16	biimpd	$⊢ (X \in A \land Y \in B) \to ((S \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C \land T \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D) \to (S \in F \land T \in G))$
18	17	imdistani	$⊢ ((X \in A \land Y \in B) \land (S \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C \land T \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D)) \to ((X \in A \land Y \in B) \land (S \in F \land T \in G))$
19	3 18	syl6	$⊢ \forall x \in A \forall y \in B (C \in U \land D \in V) \to (W \in (S (X O Y) T) \to ((X \in A \land Y \in B) \land (S \in F \land T \in G)))$

Metamath Proof Explorer

Theorem el2mpocl

Proof