Theorem oprabv 6668

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.)

Assertion

Ref	Expression
oprabv	⊢ (⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍 → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V))

Distinct variable groups:   𝑥,𝑋,𝑦,𝑧   𝑥,𝑌,𝑦,𝑧   𝑥,𝑍,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem oprabv

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		reloprab 6667	. . 3 ⊢ Rel {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
2		brrelex12 5125	. . 3 ⊢ ((Rel {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ∧ ⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍) → (⟨𝑋, 𝑌⟩ ∈ V ∧ 𝑍 ∈ V))
3	1, 2	mpan 705	. 2 ⊢ (⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍 → (⟨𝑋, 𝑌⟩ ∈ V ∧ 𝑍 ∈ V))
4		df-br 4624	. . . . 5 ⊢ (⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍 ↔ ⟨⟨𝑋, 𝑌⟩, 𝑍⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑})
5		opex 4903	. . . . . . . . 9 ⊢ ⟨𝑋, 𝑌⟩ ∈ V
6		nfcv 2761	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑤⟨𝑋, 𝑌⟩
7	6	nfeq1 2774	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩
8		nfv 1840	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑤𝜑
9	7, 8	nfan 1825	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
10	9	nfex 2151	. . . . . . . . . . 11 ⊢ Ⅎ𝑤∃𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
11	10	nfex 2151	. . . . . . . . . 10 ⊢ Ⅎ𝑤∃𝑥∃𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
12		nfcv 2761	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑧⟨𝑋, 𝑌⟩
13	12	nfeq1 2774	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩
14		nfsbc1v 3442	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧[𝑍 / 𝑧]𝜑
15	13, 14	nfan 1825	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑)
16	15	nfex 2151	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∃𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑)
17	16	nfex 2151	. . . . . . . . . 10 ⊢ Ⅎ𝑧∃𝑥∃𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑)
18		eqeq1 2625	. . . . . . . . . . . 12 ⊢ (𝑤 = ⟨𝑋, 𝑌⟩ → (𝑤 = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩))
19	18	anbi1d 740	. . . . . . . . . . 11 ⊢ (𝑤 = ⟨𝑋, 𝑌⟩ → ((𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
20	19	2exbidv 1849	. . . . . . . . . 10 ⊢ (𝑤 = ⟨𝑋, 𝑌⟩ → (∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥∃𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
21		sbceq1a 3433	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑍 → (𝜑 ↔ [𝑍 / 𝑧]𝜑))
22	21	anbi2d 739	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑍 → ((⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑)))
23	22	2exbidv 1849	. . . . . . . . . 10 ⊢ (𝑧 = 𝑍 → (∃𝑥∃𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥∃𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑)))
24	11, 17, 20, 23	opelopabgf 4965	. . . . . . . . 9 ⊢ ((⟨𝑋, 𝑌⟩ ∈ V ∧ 𝑍 ∈ V) → (⟨⟨𝑋, 𝑌⟩, 𝑍⟩ ∈ {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} ↔ ∃𝑥∃𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑)))
25	5, 24	mpan 705	. . . . . . . 8 ⊢ (𝑍 ∈ V → (⟨⟨𝑋, 𝑌⟩, 𝑍⟩ ∈ {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} ↔ ∃𝑥∃𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑)))
26		eqcom 2628	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑋, 𝑌⟩)
27		vex 3193	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
28		vex 3193	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
29	27, 28	opth 4915	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑋, 𝑌⟩ ↔ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌))
30	26, 29	bitri 264	. . . . . . . . . . . . . 14 ⊢ (⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝑥 = 𝑋 ∧ 𝑦 = 𝑌))
31		eqvisset 3201	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑋 → 𝑋 ∈ V)
32		eqvisset 3201	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑌 → 𝑌 ∈ V)
33	31, 32	anim12i 589	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V))
34	30, 33	sylbi 207	. . . . . . . . . . . . 13 ⊢ (⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ → (𝑋 ∈ V ∧ 𝑌 ∈ V))
35	34	adantr 481	. . . . . . . . . . . 12 ⊢ ((⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑) → (𝑋 ∈ V ∧ 𝑌 ∈ V))
36	35	exlimivv 1857	. . . . . . . . . . 11 ⊢ (∃𝑥∃𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑) → (𝑋 ∈ V ∧ 𝑌 ∈ V))
37	36	anim1i 591	. . . . . . . . . 10 ⊢ ((∃𝑥∃𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑) ∧ 𝑍 ∈ V) → ((𝑋 ∈ V ∧ 𝑌 ∈ V) ∧ 𝑍 ∈ V))
38		df-3an 1038	. . . . . . . . . 10 ⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V) ↔ ((𝑋 ∈ V ∧ 𝑌 ∈ V) ∧ 𝑍 ∈ V))
39	37, 38	sylibr 224	. . . . . . . . 9 ⊢ ((∃𝑥∃𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑) ∧ 𝑍 ∈ V) → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V))
40	39	expcom 451	. . . . . . . 8 ⊢ (𝑍 ∈ V → (∃𝑥∃𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑) → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)))
41	25, 40	sylbid 230	. . . . . . 7 ⊢ (𝑍 ∈ V → (⟨⟨𝑋, 𝑌⟩, 𝑍⟩ ∈ {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)))
42	41	com12 32	. . . . . 6 ⊢ (⟨⟨𝑋, 𝑌⟩, 𝑍⟩ ∈ {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} → (𝑍 ∈ V → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)))
43		dfoprab2 6666	. . . . . 6 ⊢ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
44	42, 43	eleq2s 2716	. . . . 5 ⊢ (⟨⟨𝑋, 𝑌⟩, 𝑍⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} → (𝑍 ∈ V → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)))
45	4, 44	sylbi 207	. . . 4 ⊢ (⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍 → (𝑍 ∈ V → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)))
46	45	com12 32	. . 3 ⊢ (𝑍 ∈ V → (⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍 → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)))
47	46	adantl 482	. 2 ⊢ ((⟨𝑋, 𝑌⟩ ∈ V ∧ 𝑍 ∈ V) → (⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍 → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)))
48	3, 47	mpcom 38	1 ⊢ (⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍 → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480  ∃wex 1701   ∈ wcel 1987  Vcvv 3190  [wsbc 3422  ⟨cop 4161   class class class wbr 4623  {copab 4682  Rel wrel 5089  {coprab 6616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pr 4877

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-opab 4684  df-xp 5090  df-rel 5091  df-oprab 6619

This theorem is referenced by: (None)