elovmporab

Description: Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. (Contributed by Alexander van der Vekens, 15-Jul-2018)

	Ref	Expression
Hypotheses	elovmporab.o	$⊢ O = (x \in V, y \in V ⟼ \{z \in M \| φ\})$
	elovmporab.v	$⊢ (X \in V \land Y \in V) \to M \in V$
Assertion	elovmporab	$⊢ Z \in (X O Y) \to (X \in V \land Y \in V \land Z \in M)$

Proof

Step	Hyp	Ref	Expression
1		elovmporab.o	$⊢ O = (x \in V, y \in V ⟼ \{z \in M \| φ\})$
2		elovmporab.v	$⊢ (X \in V \land Y \in V) \to M \in V$
3	1	elmpocl	$⊢ Z \in (X O Y) \to (X \in V \land Y \in V)$
4	1	a1i	$⊢ (X \in V \land Y \in V) \to O = (x \in V, y \in V ⟼ \{z \in M \| φ\})$
5		sbceq1a	$⊢ y = Y \to (φ \leftrightarrow \underset{˙}{[} Y / y \underset{˙}{]} φ)$
6		sbceq1a	$⊢ x = X \to (\underset{˙}{[} Y / y \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ)$
7	5 6	sylan9bbr	$⊢ (x = X \land y = Y) \to (φ \leftrightarrow \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ)$
8	7	adantl	$⊢ ((X \in V \land Y \in V) \land (x = X \land y = Y)) \to (φ \leftrightarrow \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ)$
9	8	rabbidv	$⊢ ((X \in V \land Y \in V) \land (x = X \land y = Y)) \to \{z \in M \| φ\} = \{z \in M \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\}$
10		eqidd	$⊢ ((X \in V \land Y \in V) \land x = X) \to V = V$
11		simpl	$⊢ (X \in V \land Y \in V) \to X \in V$
12		simpr	$⊢ (X \in V \land Y \in V) \to Y \in V$
13		rabexg	$⊢ M \in V \to \{z \in M \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\} \in V$
14	2 13	syl	$⊢ (X \in V \land Y \in V) \to \{z \in M \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\} \in V$
15		nfcv	$⊢ \underline{Ⅎ} x X$
16	15	nfel1	$⊢ Ⅎ x X \in V$
17		nfcv	$⊢ \underline{Ⅎ} x Y$
18	17	nfel1	$⊢ Ⅎ x Y \in V$
19	16 18	nfan	$⊢ Ⅎ x (X \in V \land Y \in V)$
20		nfcv	$⊢ \underline{Ⅎ} y X$
21	20	nfel1	$⊢ Ⅎ y X \in V$
22		nfcv	$⊢ \underline{Ⅎ} y Y$
23	22	nfel1	$⊢ Ⅎ y Y \in V$
24	21 23	nfan	$⊢ Ⅎ y (X \in V \land Y \in V)$
25		nfsbc1v	$⊢ Ⅎ x \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ$
26		nfcv	$⊢ \underline{Ⅎ} x M$
27	25 26	nfrabw	$⊢ \underline{Ⅎ} x \{z \in M \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\}$
28		nfsbc1v	$⊢ Ⅎ y \underset{˙}{[} Y / y \underset{˙}{]} φ$
29	20 28	nfsbcw	$⊢ Ⅎ y \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ$
30		nfcv	$⊢ \underline{Ⅎ} y M$
31	29 30	nfrabw	$⊢ \underline{Ⅎ} y \{z \in M \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\}$
32	4 9 10 11 12 14 19 24 20 17 27 31	ovmpodxf	$⊢ (X \in V \land Y \in V) \to X O Y = \{z \in M \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\}$
33	32	eleq2d	$⊢ (X \in V \land Y \in V) \to (Z \in (X O Y) \leftrightarrow Z \in \{z \in M \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\})$
34		df-3an	$⊢ (X \in V \land Y \in V \land Z \in M) \leftrightarrow ((X \in V \land Y \in V) \land Z \in M)$
35	34	simplbi2com	$⊢ Z \in M \to ((X \in V \land Y \in V) \to (X \in V \land Y \in V \land Z \in M))$
36		elrabi	$⊢ Z \in \{z \in M \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\} \to Z \in M$
37	35 36	syl11	$⊢ (X \in V \land Y \in V) \to (Z \in \{z \in M \| \underset{˙}{[} X / x \underset{˙}{]} \underset{˙}{[} Y / y \underset{˙}{]} φ\} \to (X \in V \land Y \in V \land Z \in M))$
38	33 37	sylbid	$⊢ (X \in V \land Y \in V) \to (Z \in (X O Y) \to (X \in V \land Y \in V \land Z \in M))$
39	3 38	mpcom	$⊢ Z \in (X O Y) \to (X \in V \land Y \in V \land Z \in M)$

Metamath Proof Explorer

Theorem elovmporab

Proof