el2mpocsbcl

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
	Hypothesis	el2mpocsbcl.o	$⊢ O = (x \in A, y \in B ⟼ (s \in C, t \in D ⟼ E))$
	Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		el2mpocsbcl.o	$⊢ O = (x \in A, y \in B ⟼ (s \in C, t \in D ⟼ E))$
2		simpl	$⊢ ((X \in A \land Y \in B) \land (\forall x \in A \forall y \in B (C \in U \land D \in V) \land W \in (S (X O Y) T))) \to (X \in A \land Y \in B)$
3		nfcv	$⊢ \underline{Ⅎ} a (s \in C, t \in D ⟼ E)$
4		nfcv	$⊢ \underline{Ⅎ} b (s \in C, t \in D ⟼ E)$
5		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ a / x ⦌ ⦋ b / y ⦌ C$
6		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ a / x ⦌ ⦋ b / y ⦌ D$
7		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ a / x ⦌ ⦋ b / y ⦌ E$
8	5 6 7	nfmpo	$⊢ \underline{Ⅎ} x (s \in ⦋ a / x ⦌ ⦋ b / y ⦌ C, t \in ⦋ a / x ⦌ ⦋ b / y ⦌ D ⟼ ⦋ a / x ⦌ ⦋ b / y ⦌ E)$
9		nfcv	$⊢ \underline{Ⅎ} y a$
10		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ b / y ⦌ C$
11	9 10	nfcsbw	$⊢ \underline{Ⅎ} y ⦋ a / x ⦌ ⦋ b / y ⦌ C$
12		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ b / y ⦌ D$
13	9 12	nfcsbw	$⊢ \underline{Ⅎ} y ⦋ a / x ⦌ ⦋ b / y ⦌ D$
14		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ b / y ⦌ E$
15	9 14	nfcsbw	$⊢ \underline{Ⅎ} y ⦋ a / x ⦌ ⦋ b / y ⦌ E$
16	11 13 15	nfmpo	$⊢ \underline{Ⅎ} y (s \in ⦋ a / x ⦌ ⦋ b / y ⦌ C, t \in ⦋ a / x ⦌ ⦋ b / y ⦌ D ⟼ ⦋ a / x ⦌ ⦋ b / y ⦌ E)$
17		csbeq1a	$⊢ x = a \to C = ⦋ a / x ⦌ C$
18		csbeq1a	$⊢ y = b \to C = ⦋ b / y ⦌ C$
19	18	csbeq2dv	$⊢ y = b \to ⦋ a / x ⦌ C = ⦋ a / x ⦌ ⦋ b / y ⦌ C$
20	17 19	sylan9eq	$⊢ (x = a \land y = b) \to C = ⦋ a / x ⦌ ⦋ b / y ⦌ C$
21		csbeq1a	$⊢ x = a \to D = ⦋ a / x ⦌ D$
22		csbeq1a	$⊢ y = b \to D = ⦋ b / y ⦌ D$
23	22	csbeq2dv	$⊢ y = b \to ⦋ a / x ⦌ D = ⦋ a / x ⦌ ⦋ b / y ⦌ D$
24	21 23	sylan9eq	$⊢ (x = a \land y = b) \to D = ⦋ a / x ⦌ ⦋ b / y ⦌ D$
25		csbeq1a	$⊢ x = a \to E = ⦋ a / x ⦌ E$
26		csbeq1a	$⊢ y = b \to E = ⦋ b / y ⦌ E$
27	26	csbeq2dv	$⊢ y = b \to ⦋ a / x ⦌ E = ⦋ a / x ⦌ ⦋ b / y ⦌ E$
28	25 27	sylan9eq	$⊢ (x = a \land y = b) \to E = ⦋ a / x ⦌ ⦋ b / y ⦌ E$
29	20 24 28	mpoeq123dv	$⊢ (x = a \land y = b) \to (s \in C, t \in D ⟼ E) = (s \in ⦋ a / x ⦌ ⦋ b / y ⦌ C, t \in ⦋ a / x ⦌ ⦋ b / y ⦌ D ⟼ ⦋ a / x ⦌ ⦋ b / y ⦌ E)$
30	3 4 8 16 29	cbvmpo	$⊢ (x \in A, y \in B ⟼ (s \in C, t \in D ⟼ E)) = (a \in A, b \in B ⟼ (s \in ⦋ a / x ⦌ ⦋ b / y ⦌ C, t \in ⦋ a / x ⦌ ⦋ b / y ⦌ D ⟼ ⦋ a / x ⦌ ⦋ b / y ⦌ E))$
31	1 30	eqtri	$⊢ O = (a \in A, b \in B ⟼ (s \in ⦋ a / x ⦌ ⦋ b / y ⦌ C, t \in ⦋ a / x ⦌ ⦋ b / y ⦌ D ⟼ ⦋ a / x ⦌ ⦋ b / y ⦌ E))$
32	31	a1i	$⊢ (\forall x \in A \forall y \in B (C \in U \land D \in V) \land (X \in A \land Y \in B)) \to O = (a \in A, b \in B ⟼ (s \in ⦋ a / x ⦌ ⦋ b / y ⦌ C, t \in ⦋ a / x ⦌ ⦋ b / y ⦌ D ⟼ ⦋ a / x ⦌ ⦋ b / y ⦌ E))$
33		csbeq1	$⊢ a = X \to ⦋ a / x ⦌ ⦋ b / y ⦌ C = ⦋ X / x ⦌ ⦋ b / y ⦌ C$
34	33	adantr	$⊢ (a = X \land b = Y) \to ⦋ a / x ⦌ ⦋ b / y ⦌ C = ⦋ X / x ⦌ ⦋ b / y ⦌ C$
35		csbeq1	$⊢ b = Y \to ⦋ b / y ⦌ C = ⦋ Y / y ⦌ C$
36	35	adantl	$⊢ (a = X \land b = Y) \to ⦋ b / y ⦌ C = ⦋ Y / y ⦌ C$
37	36	csbeq2dv	$⊢ (a = X \land b = Y) \to ⦋ X / x ⦌ ⦋ b / y ⦌ C = ⦋ X / x ⦌ ⦋ Y / y ⦌ C$
38	34 37	eqtrd	$⊢ (a = X \land b = Y) \to ⦋ a / x ⦌ ⦋ b / y ⦌ C = ⦋ X / x ⦌ ⦋ Y / y ⦌ C$
39		csbeq1	$⊢ a = X \to ⦋ a / x ⦌ ⦋ b / y ⦌ D = ⦋ X / x ⦌ ⦋ b / y ⦌ D$
40	39	adantr	$⊢ (a = X \land b = Y) \to ⦋ a / x ⦌ ⦋ b / y ⦌ D = ⦋ X / x ⦌ ⦋ b / y ⦌ D$
41		csbeq1	$⊢ b = Y \to ⦋ b / y ⦌ D = ⦋ Y / y ⦌ D$
42	41	adantl	$⊢ (a = X \land b = Y) \to ⦋ b / y ⦌ D = ⦋ Y / y ⦌ D$
43	42	csbeq2dv	$⊢ (a = X \land b = Y) \to ⦋ X / x ⦌ ⦋ b / y ⦌ D = ⦋ X / x ⦌ ⦋ Y / y ⦌ D$
44	40 43	eqtrd	$⊢ (a = X \land b = Y) \to ⦋ a / x ⦌ ⦋ b / y ⦌ D = ⦋ X / x ⦌ ⦋ Y / y ⦌ D$
45		csbeq1	$⊢ a = X \to ⦋ a / x ⦌ ⦋ b / y ⦌ E = ⦋ X / x ⦌ ⦋ b / y ⦌ E$
46	45	adantr	$⊢ (a = X \land b = Y) \to ⦋ a / x ⦌ ⦋ b / y ⦌ E = ⦋ X / x ⦌ ⦋ b / y ⦌ E$
47		csbeq1	$⊢ b = Y \to ⦋ b / y ⦌ E = ⦋ Y / y ⦌ E$
48	47	adantl	$⊢ (a = X \land b = Y) \to ⦋ b / y ⦌ E = ⦋ Y / y ⦌ E$
49	48	csbeq2dv	$⊢ (a = X \land b = Y) \to ⦋ X / x ⦌ ⦋ b / y ⦌ E = ⦋ X / x ⦌ ⦋ Y / y ⦌ E$
50	46 49	eqtrd	$⊢ (a = X \land b = Y) \to ⦋ a / x ⦌ ⦋ b / y ⦌ E = ⦋ X / x ⦌ ⦋ Y / y ⦌ E$
51	38 44 50	mpoeq123dv	$⊢ (a = X \land b = Y) \to (s \in ⦋ a / x ⦌ ⦋ b / y ⦌ C, t \in ⦋ a / x ⦌ ⦋ b / y ⦌ D ⟼ ⦋ a / x ⦌ ⦋ b / y ⦌ E) = (s \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C, t \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D ⟼ ⦋ X / x ⦌ ⦋ Y / y ⦌ E)$
52	51	adantl	$⊢ ((\forall x \in A \forall y \in B (C \in U \land D \in V) \land (X \in A \land Y \in B)) \land (a = X \land b = Y)) \to (s \in ⦋ a / x ⦌ ⦋ b / y ⦌ C, t \in ⦋ a / x ⦌ ⦋ b / y ⦌ D ⟼ ⦋ a / x ⦌ ⦋ b / y ⦌ E) = (s \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C, t \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D ⟼ ⦋ X / x ⦌ ⦋ Y / y ⦌ E)$
53		simpl	$⊢ (X \in A \land Y \in B) \to X \in A$
54	53	adantl	$⊢ (\forall x \in A \forall y \in B (C \in U \land D \in V) \land (X \in A \land Y \in B)) \to X \in A$
55		simpr	$⊢ (X \in A \land Y \in B) \to Y \in B$
56	55	adantl	$⊢ (\forall x \in A \forall y \in B (C \in U \land D \in V) \land (X \in A \land Y \in B)) \to Y \in B$
57		simpl	$⊢ (C \in U \land D \in V) \to C \in U$
58	57	ralimi	$⊢ \forall y \in B (C \in U \land D \in V) \to \forall y \in B C \in U$
59		rspcsbela	$⊢ (Y \in B \land \forall y \in B C \in U) \to ⦋ Y / y ⦌ C \in U$
60	55 58 59	syl2an	$⊢ ((X \in A \land Y \in B) \land \forall y \in B (C \in U \land D \in V)) \to ⦋ Y / y ⦌ C \in U$
61	60	ex	$⊢ (X \in A \land Y \in B) \to (\forall y \in B (C \in U \land D \in V) \to ⦋ Y / y ⦌ C \in U)$
62	61	ralimdv	$⊢ (X \in A \land Y \in B) \to (\forall x \in A \forall y \in B (C \in U \land D \in V) \to \forall x \in A ⦋ Y / y ⦌ C \in U)$
63	62	impcom	$⊢ (\forall x \in A \forall y \in B (C \in U \land D \in V) \land (X \in A \land Y \in B)) \to \forall x \in A ⦋ Y / y ⦌ C \in U$
64		rspcsbela	$⊢ (X \in A \land \forall x \in A ⦋ Y / y ⦌ C \in U) \to ⦋ X / x ⦌ ⦋ Y / y ⦌ C \in U$
65	54 63 64	syl2anc	$⊢ (\forall x \in A \forall y \in B (C \in U \land D \in V) \land (X \in A \land Y \in B)) \to ⦋ X / x ⦌ ⦋ Y / y ⦌ C \in U$
66		simpr	$⊢ (C \in U \land D \in V) \to D \in V$
67	66	ralimi	$⊢ \forall y \in B (C \in U \land D \in V) \to \forall y \in B D \in V$
68		rspcsbela	$⊢ (Y \in B \land \forall y \in B D \in V) \to ⦋ Y / y ⦌ D \in V$
69	55 67 68	syl2an	$⊢ ((X \in A \land Y \in B) \land \forall y \in B (C \in U \land D \in V)) \to ⦋ Y / y ⦌ D \in V$
70	69	ex	$⊢ (X \in A \land Y \in B) \to (\forall y \in B (C \in U \land D \in V) \to ⦋ Y / y ⦌ D \in V)$
71	70	ralimdv	$⊢ (X \in A \land Y \in B) \to (\forall x \in A \forall y \in B (C \in U \land D \in V) \to \forall x \in A ⦋ Y / y ⦌ D \in V)$
72	71	impcom	$⊢ (\forall x \in A \forall y \in B (C \in U \land D \in V) \land (X \in A \land Y \in B)) \to \forall x \in A ⦋ Y / y ⦌ D \in V$
73		rspcsbela	$⊢ (X \in A \land \forall x \in A ⦋ Y / y ⦌ D \in V) \to ⦋ X / x ⦌ ⦋ Y / y ⦌ D \in V$
74	54 72 73	syl2anc	$⊢ (\forall x \in A \forall y \in B (C \in U \land D \in V) \land (X \in A \land Y \in B)) \to ⦋ X / x ⦌ ⦋ Y / y ⦌ D \in V$
75		mpoexga	$⊢ (⦋ X / x ⦌ ⦋ Y / y ⦌ C \in U \land ⦋ X / x ⦌ ⦋ Y / y ⦌ D \in V) \to (s \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C, t \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D ⟼ ⦋ X / x ⦌ ⦋ Y / y ⦌ E) \in V$
76	65 74 75	syl2anc	$⊢ (\forall x \in A \forall y \in B (C \in U \land D \in V) \land (X \in A \land Y \in B)) \to (s \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C, t \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D ⟼ ⦋ X / x ⦌ ⦋ Y / y ⦌ E) \in V$
77	32 52 54 56 76	ovmpod	$⊢ (\forall x \in A \forall y \in B (C \in U \land D \in V) \land (X \in A \land Y \in B)) \to X O Y = (s \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C, t \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D ⟼ ⦋ X / x ⦌ ⦋ Y / y ⦌ E)$
78	77	oveqd	$⊢ (\forall x \in A \forall y \in B (C \in U \land D \in V) \land (X \in A \land Y \in B)) \to S (X O Y) T = S (s \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C, t \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D ⟼ ⦋ X / x ⦌ ⦋ Y / y ⦌ E) T$
79	78	eleq2d	$⊢ (\forall x \in A \forall y \in B (C \in U \land D \in V) \land (X \in A \land Y \in B)) \to (W \in (S (X O Y) T) \leftrightarrow W \in (S (s \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C, t \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D ⟼ ⦋ X / x ⦌ ⦋ Y / y ⦌ E) T))$
80		eqid	$⊢ (s \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C, t \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D ⟼ ⦋ X / x ⦌ ⦋ Y / y ⦌ E) = (s \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C, t \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D ⟼ ⦋ X / x ⦌ ⦋ Y / y ⦌ E)$
81	80	elmpocl	$⊢ W \in (S (s \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C, t \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D ⟼ ⦋ X / x ⦌ ⦋ Y / y ⦌ E) T) \to (S \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C \land T \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D)$
82	79 81	biimtrdi	$⊢ (\forall x \in A \forall y \in B (C \in U \land D \in V) \land (X \in A \land Y \in B)) \to (W \in (S (X O Y) T) \to (S \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C \land T \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D))$
83	82	impancom	$⊢ (\forall x \in A \forall y \in B (C \in U \land D \in V) \land W \in (S (X O Y) T)) \to ((X \in A \land Y \in B) \to (S \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C \land T \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D))$
84	83	impcom	$⊢ ((X \in A \land Y \in B) \land (\forall x \in A \forall y \in B (C \in U \land D \in V) \land W \in (S (X O Y) T))) \to (S \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C \land T \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D)$
85	2 84	jca	$⊢ ((X \in A \land Y \in B) \land (\forall x \in A \forall y \in B (C \in U \land D \in V) \land 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))$
86	85	ex	$⊢ (X \in A \land Y \in B) \to ((\forall x \in A \forall y \in B (C \in U \land D \in V) \land 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)))$
87	1	mpondm0	$⊢ \neg (X \in A \land Y \in B) \to X O Y = \emptyset$
88	87	oveqd	$⊢ \neg (X \in A \land Y \in B) \to S (X O Y) T = S \emptyset T$
89	88	eleq2d	$⊢ \neg (X \in A \land Y \in B) \to (W \in (S (X O Y) T) \leftrightarrow W \in (S \emptyset T))$
90		noel	$⊢ \neg W \in \emptyset$
91	90	pm2.21i	$⊢ W \in \emptyset \to ((X \in A \land Y \in B) \land (S \in ⦋ X / x ⦌ ⦋ Y / y ⦌ C \land T \in ⦋ X / x ⦌ ⦋ Y / y ⦌ D))$
92		0ov	$⊢ S \emptyset T = \emptyset$
93	91 92	eleq2s	$⊢ W \in (S \emptyset 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))$
94	89 93	biimtrdi	$⊢ \neg (X \in A \land Y \in B) \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)))$
95	94	adantld	$⊢ \neg (X \in A \land Y \in B) \to ((\forall x \in A \forall y \in B (C \in U \land D \in V) \land 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)))$
96	86 95	pm2.61i	$⊢ (\forall x \in A \forall y \in B (C \in U \land D \in V) \land 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))$
97	96	ex	$⊢ \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)))$

Metamath Proof Explorer

Theorem el2mpocsbcl

Proof