oprabv

Description: If a pair and a class are in a relationship given by a class abstraction of a collection of nested ordered pairs, the involved classes are sets. (Contributed by Alexander van der Vekens, 8-Jul-2018)

		Ref	Expression
	Assertion	oprabv	$⊢ ⟨X, Y⟩ \{⟨⟨x, y⟩, z⟩ \| φ\} Z \to (X \in V \land Y \in V \land Z \in V)$

Proof

Step	Hyp	Ref	Expression
1		reloprab	$⊢ Rel \{⟨⟨x, y⟩, z⟩ \| φ\}$
2	1	brrelex12i	$⊢ ⟨X, Y⟩ \{⟨⟨x, y⟩, z⟩ \| φ\} Z \to (⟨X, Y⟩ \in V \land Z \in V)$
3		df-br	$⊢ ⟨X, Y⟩ \{⟨⟨x, y⟩, z⟩ \| φ\} Z \leftrightarrow ⟨⟨X, Y⟩, Z⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\}$
4		opex	$⊢ ⟨X, Y⟩ \in V$
5		nfcv	$⊢ \underline{Ⅎ} w ⟨X, Y⟩$
6	5	nfeq1	$⊢ Ⅎ w ⟨X, Y⟩ = ⟨x, y⟩$
7		nfv	$⊢ Ⅎ w φ$
8	6 7	nfan	$⊢ Ⅎ w (⟨X, Y⟩ = ⟨x, y⟩ \land φ)$
9	8	nfex	$⊢ Ⅎ w \exists y (⟨X, Y⟩ = ⟨x, y⟩ \land φ)$
10	9	nfex	$⊢ Ⅎ w \exists x \exists y (⟨X, Y⟩ = ⟨x, y⟩ \land φ)$
11		nfcv	$⊢ \underline{Ⅎ} z ⟨X, Y⟩$
12	11	nfeq1	$⊢ Ⅎ z ⟨X, Y⟩ = ⟨x, y⟩$
13		nfsbc1v	$⊢ Ⅎ z \underset{˙}{[} Z / z \underset{˙}{]} φ$
14	12 13	nfan	$⊢ Ⅎ z (⟨X, Y⟩ = ⟨x, y⟩ \land \underset{˙}{[} Z / z \underset{˙}{]} φ)$
15	14	nfex	$⊢ Ⅎ z \exists y (⟨X, Y⟩ = ⟨x, y⟩ \land \underset{˙}{[} Z / z \underset{˙}{]} φ)$
16	15	nfex	$⊢ Ⅎ z \exists x \exists y (⟨X, Y⟩ = ⟨x, y⟩ \land \underset{˙}{[} Z / z \underset{˙}{]} φ)$
17		eqeq1	$⊢ w = ⟨X, Y⟩ \to (w = ⟨x, y⟩ \leftrightarrow ⟨X, Y⟩ = ⟨x, y⟩)$
18	17	anbi1d	$⊢ w = ⟨X, Y⟩ \to ((w = ⟨x, y⟩ \land φ) \leftrightarrow (⟨X, Y⟩ = ⟨x, y⟩ \land φ))$
19	18	2exbidv	$⊢ w = ⟨X, Y⟩ \to (\exists x \exists y (w = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y (⟨X, Y⟩ = ⟨x, y⟩ \land φ))$
20		sbceq1a	$⊢ z = Z \to (φ \leftrightarrow \underset{˙}{[} Z / z \underset{˙}{]} φ)$
21	20	anbi2d	$⊢ z = Z \to ((⟨X, Y⟩ = ⟨x, y⟩ \land φ) \leftrightarrow (⟨X, Y⟩ = ⟨x, y⟩ \land \underset{˙}{[} Z / z \underset{˙}{]} φ))$
22	21	2exbidv	$⊢ z = Z \to (\exists x \exists y (⟨X, Y⟩ = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y (⟨X, Y⟩ = ⟨x, y⟩ \land \underset{˙}{[} Z / z \underset{˙}{]} φ))$
23	10 16 19 22	opelopabgf	$⊢ (⟨X, Y⟩ \in V \land Z \in V) \to (⟨⟨X, Y⟩, Z⟩ \in \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} \leftrightarrow \exists x \exists y (⟨X, Y⟩ = ⟨x, y⟩ \land \underset{˙}{[} Z / z \underset{˙}{]} φ))$
24	4 23	mpan	$⊢ Z \in V \to (⟨⟨X, Y⟩, Z⟩ \in \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} \leftrightarrow \exists x \exists y (⟨X, Y⟩ = ⟨x, y⟩ \land \underset{˙}{[} Z / z \underset{˙}{]} φ))$
25		eqcom	$⊢ ⟨X, Y⟩ = ⟨x, y⟩ \leftrightarrow ⟨x, y⟩ = ⟨X, Y⟩$
26		vex	$⊢ x \in V$
27		vex	$⊢ y \in V$
28	26 27	opth	$⊢ ⟨x, y⟩ = ⟨X, Y⟩ \leftrightarrow (x = X \land y = Y)$
29	25 28	bitri	$⊢ ⟨X, Y⟩ = ⟨x, y⟩ \leftrightarrow (x = X \land y = Y)$
30		eqvisset	$⊢ x = X \to X \in V$
31		eqvisset	$⊢ y = Y \to Y \in V$
32	30 31	anim12i	$⊢ (x = X \land y = Y) \to (X \in V \land Y \in V)$
33	29 32	sylbi	$⊢ ⟨X, Y⟩ = ⟨x, y⟩ \to (X \in V \land Y \in V)$
34	33	adantr	$⊢ (⟨X, Y⟩ = ⟨x, y⟩ \land \underset{˙}{[} Z / z \underset{˙}{]} φ) \to (X \in V \land Y \in V)$
35	34	exlimivv	$⊢ \exists x \exists y (⟨X, Y⟩ = ⟨x, y⟩ \land \underset{˙}{[} Z / z \underset{˙}{]} φ) \to (X \in V \land Y \in V)$
36	35	anim1i	$⊢ (\exists x \exists y (⟨X, Y⟩ = ⟨x, y⟩ \land \underset{˙}{[} Z / z \underset{˙}{]} φ) \land Z \in V) \to ((X \in V \land Y \in V) \land Z \in V)$
37		df-3an	$⊢ (X \in V \land Y \in V \land Z \in V) \leftrightarrow ((X \in V \land Y \in V) \land Z \in V)$
38	36 37	sylibr	$⊢ (\exists x \exists y (⟨X, Y⟩ = ⟨x, y⟩ \land \underset{˙}{[} Z / z \underset{˙}{]} φ) \land Z \in V) \to (X \in V \land Y \in V \land Z \in V)$
39	38	expcom	$⊢ Z \in V \to (\exists x \exists y (⟨X, Y⟩ = ⟨x, y⟩ \land \underset{˙}{[} Z / z \underset{˙}{]} φ) \to (X \in V \land Y \in V \land Z \in V))$
40	24 39	sylbid	$⊢ Z \in V \to (⟨⟨X, Y⟩, Z⟩ \in \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} \to (X \in V \land Y \in V \land Z \in V))$
41	40	com12	$⊢ ⟨⟨X, Y⟩, Z⟩ \in \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\} \to (Z \in V \to (X \in V \land Y \in V \land Z \in V))$
42		dfoprab2	$⊢ \{⟨⟨x, y⟩, z⟩ \| φ\} = \{⟨w, z⟩ \| \exists x \exists y (w = ⟨x, y⟩ \land φ)\}$
43	41 42	eleq2s	$⊢ ⟨⟨X, Y⟩, Z⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \to (Z \in V \to (X \in V \land Y \in V \land Z \in V))$
44	3 43	sylbi	$⊢ ⟨X, Y⟩ \{⟨⟨x, y⟩, z⟩ \| φ\} Z \to (Z \in V \to (X \in V \land Y \in V \land Z \in V))$
45	44	com12	$⊢ Z \in V \to (⟨X, Y⟩ \{⟨⟨x, y⟩, z⟩ \| φ\} Z \to (X \in V \land Y \in V \land Z \in V))$
46	45	adantl	$⊢ (⟨X, Y⟩ \in V \land Z \in V) \to (⟨X, Y⟩ \{⟨⟨x, y⟩, z⟩ \| φ\} Z \to (X \in V \land Y \in V \land Z \in V))$
47	2 46	mpcom	$⊢ ⟨X, Y⟩ \{⟨⟨x, y⟩, z⟩ \| φ\} Z \to (X \in V \land Y \in V \land Z \in V)$

Metamath Proof Explorer

Theorem oprabv

Proof