elrnmpores

Description: Membership in the range of a restricted operation class abstraction. (Contributed by Thierry Arnoux, 25-May-2019)

		Ref	Expression
	Hypothesis	rngop.1	$⊢ F = (x \in A, y \in B ⟼ C)$
	Assertion	elrnmpores	$⊢ D \in V \to (D \in ran ({F ↾}_{R}) \leftrightarrow \exists x \in A \exists y \in B (D = C \land x R y))$

Proof

Step	Hyp	Ref	Expression
1		rngop.1	$⊢ F = (x \in A, y \in B ⟼ C)$
2		eqeq1	$⊢ z = D \to (z = C \leftrightarrow D = C)$
3	2	anbi1d	$⊢ z = D \to ((z = C \land x R y) \leftrightarrow (D = C \land x R y))$
4	3	anbi2d	$⊢ z = D \to (((x \in A \land y \in B) \land (z = C \land x R y)) \leftrightarrow ((x \in A \land y \in B) \land (D = C \land x R y)))$
5	4	2exbidv	$⊢ z = D \to (\exists x \exists y ((x \in A \land y \in B) \land (z = C \land x R y)) \leftrightarrow \exists x \exists y ((x \in A \land y \in B) \land (D = C \land x R y)))$
6		an12	$⊢ (p \in R \land (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C))) \leftrightarrow (p = ⟨x, y⟩ \land (p \in R \land ((x \in A \land y \in B) \land z = C)))$
7		an12	$⊢ (p \in R \land ((x \in A \land y \in B) \land z = C)) \leftrightarrow ((x \in A \land y \in B) \land (p \in R \land z = C))$
8		ancom	$⊢ (z = C \land p \in R) \leftrightarrow (p \in R \land z = C)$
9		eleq1	$⊢ p = ⟨x, y⟩ \to (p \in R \leftrightarrow ⟨x, y⟩ \in R)$
10		df-br	$⊢ x R y \leftrightarrow ⟨x, y⟩ \in R$
11	9 10	bitr4di	$⊢ p = ⟨x, y⟩ \to (p \in R \leftrightarrow x R y)$
12	11	anbi2d	$⊢ p = ⟨x, y⟩ \to ((z = C \land p \in R) \leftrightarrow (z = C \land x R y))$
13	8 12	bitr3id	$⊢ p = ⟨x, y⟩ \to ((p \in R \land z = C) \leftrightarrow (z = C \land x R y))$
14	13	anbi2d	$⊢ p = ⟨x, y⟩ \to (((x \in A \land y \in B) \land (p \in R \land z = C)) \leftrightarrow ((x \in A \land y \in B) \land (z = C \land x R y)))$
15	7 14	bitrid	$⊢ p = ⟨x, y⟩ \to ((p \in R \land ((x \in A \land y \in B) \land z = C)) \leftrightarrow ((x \in A \land y \in B) \land (z = C \land x R y)))$
16	15	pm5.32i	$⊢ (p = ⟨x, y⟩ \land (p \in R \land ((x \in A \land y \in B) \land z = C))) \leftrightarrow (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land (z = C \land x R y)))$
17	6 16	bitri	$⊢ (p \in R \land (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C))) \leftrightarrow (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land (z = C \land x R y)))$
18	17	2exbii	$⊢ \exists x \exists y (p \in R \land (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C))) \leftrightarrow \exists x \exists y (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land (z = C \land x R y)))$
19		19.42vv	$⊢ \exists x \exists y (p \in R \land (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C))) \leftrightarrow (p \in R \land \exists x \exists y (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)))$
20	18 19	bitr3i	$⊢ \exists x \exists y (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land (z = C \land x R y))) \leftrightarrow (p \in R \land \exists x \exists y (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)))$
21	20	opabbii	$⊢ \{⟨p, z⟩ \| \exists x \exists y (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land (z = C \land x R y)))\} = \{⟨p, z⟩ \| (p \in R \land \exists x \exists y (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)))\}$
22		dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land (z = C \land x R y))\} = \{⟨p, z⟩ \| \exists x \exists y (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land (z = C \land x R y)))\}$
23		df-mpo	$⊢ (x \in A, y \in B ⟼ C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\}$
24		dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land z = C)\} = \{⟨p, z⟩ \| \exists x \exists y (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C))\}$
25	1 23 24	3eqtri	$⊢ F = \{⟨p, z⟩ \| \exists x \exists y (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C))\}$
26	25	reseq1i	$⊢ {F ↾}_{R} = {\{⟨p, z⟩ \| \exists x \exists y (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C))\} ↾}_{R}$
27		resopab	$⊢ {\{⟨p, z⟩ \| \exists x \exists y (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C))\} ↾}_{R} = \{⟨p, z⟩ \| (p \in R \land \exists x \exists y (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)))\}$
28	26 27	eqtri	$⊢ {F ↾}_{R} = \{⟨p, z⟩ \| (p \in R \land \exists x \exists y (p = ⟨x, y⟩ \land ((x \in A \land y \in B) \land z = C)))\}$
29	21 22 28	3eqtr4ri	$⊢ {F ↾}_{R} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land (z = C \land x R y))\}$
30	29	rneqi	$⊢ ran ({F ↾}_{R}) = ran \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land (z = C \land x R y))\}$
31		rnoprab	$⊢ ran \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land (z = C \land x R y))\} = \{z \| \exists x \exists y ((x \in A \land y \in B) \land (z = C \land x R y))\}$
32	30 31	eqtri	$⊢ ran ({F ↾}_{R}) = \{z \| \exists x \exists y ((x \in A \land y \in B) \land (z = C \land x R y))\}$
33	5 32	elab2g	$⊢ D \in V \to (D \in ran ({F ↾}_{R}) \leftrightarrow \exists x \exists y ((x \in A \land y \in B) \land (D = C \land x R y)))$
34		r2ex	$⊢ \exists x \in A \exists y \in B (D = C \land x R y) \leftrightarrow \exists x \exists y ((x \in A \land y \in B) \land (D = C \land x R y))$
35	33 34	bitr4di	$⊢ D \in V \to (D \in ran ({F ↾}_{R}) \leftrightarrow \exists x \in A \exists y \in B (D = C \land x R y))$

Metamath Proof Explorer

Theorem elrnmpores

Proof