MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oprabv Structured version   Visualization version   GIF version

Theorem oprabv 6905
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.
StepHypRef Expression
1 reloprab 6904 . . 3 Rel {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}
21brrelex12i 5329 . 2 (⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍 → (⟨𝑋, 𝑌⟩ ∈ V ∧ 𝑍 ∈ V))
3 df-br 4812 . . . . 5 (⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍 ↔ ⟨⟨𝑋, 𝑌⟩, 𝑍⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑})
4 opex 5090 . . . . . . . . 9 𝑋, 𝑌⟩ ∈ V
5 nfcv 2907 . . . . . . . . . . . . . 14 𝑤𝑋, 𝑌
65nfeq1 2921 . . . . . . . . . . . . 13 𝑤𝑋, 𝑌⟩ = ⟨𝑥, 𝑦
7 nfv 2009 . . . . . . . . . . . . 13 𝑤𝜑
86, 7nfan 1998 . . . . . . . . . . . 12 𝑤(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
98nfex 2327 . . . . . . . . . . 11 𝑤𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
109nfex 2327 . . . . . . . . . 10 𝑤𝑥𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
11 nfcv 2907 . . . . . . . . . . . . . 14 𝑧𝑋, 𝑌
1211nfeq1 2921 . . . . . . . . . . . . 13 𝑧𝑋, 𝑌⟩ = ⟨𝑥, 𝑦
13 nfsbc1v 3618 . . . . . . . . . . . . 13 𝑧[𝑍 / 𝑧]𝜑
1412, 13nfan 1998 . . . . . . . . . . . 12 𝑧(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑)
1514nfex 2327 . . . . . . . . . . 11 𝑧𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑)
1615nfex 2327 . . . . . . . . . 10 𝑧𝑥𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑)
17 eqeq1 2769 . . . . . . . . . . . 12 (𝑤 = ⟨𝑋, 𝑌⟩ → (𝑤 = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩))
1817anbi1d 623 . . . . . . . . . . 11 (𝑤 = ⟨𝑋, 𝑌⟩ → ((𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
19182exbidv 2019 . . . . . . . . . 10 (𝑤 = ⟨𝑋, 𝑌⟩ → (∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
20 sbceq1a 3609 . . . . . . . . . . . 12 (𝑧 = 𝑍 → (𝜑[𝑍 / 𝑧]𝜑))
2120anbi2d 622 . . . . . . . . . . 11 (𝑧 = 𝑍 → ((⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑)))
22212exbidv 2019 . . . . . . . . . 10 (𝑧 = 𝑍 → (∃𝑥𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑥𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑)))
2310, 16, 19, 22opelopabgf 5158 . . . . . . . . 9 ((⟨𝑋, 𝑌⟩ ∈ V ∧ 𝑍 ∈ V) → (⟨⟨𝑋, 𝑌⟩, 𝑍⟩ ∈ {⟨𝑤, 𝑧⟩ ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} ↔ ∃𝑥𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑)))
244, 23mpan 681 . . . . . . . 8 (𝑍 ∈ V → (⟨⟨𝑋, 𝑌⟩, 𝑍⟩ ∈ {⟨𝑤, 𝑧⟩ ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} ↔ ∃𝑥𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑)))
25 eqcom 2772 . . . . . . . . . . . . . . 15 (⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ↔ ⟨𝑥, 𝑦⟩ = ⟨𝑋, 𝑌⟩)
26 vex 3353 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
27 vex 3353 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
2826, 27opth 5102 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ = ⟨𝑋, 𝑌⟩ ↔ (𝑥 = 𝑋𝑦 = 𝑌))
2925, 28bitri 266 . . . . . . . . . . . . . 14 (⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ↔ (𝑥 = 𝑋𝑦 = 𝑌))
30 eqvisset 3364 . . . . . . . . . . . . . . 15 (𝑥 = 𝑋𝑋 ∈ V)
31 eqvisset 3364 . . . . . . . . . . . . . . 15 (𝑦 = 𝑌𝑌 ∈ V)
3230, 31anim12i 606 . . . . . . . . . . . . . 14 ((𝑥 = 𝑋𝑦 = 𝑌) → (𝑋 ∈ V ∧ 𝑌 ∈ V))
3329, 32sylbi 208 . . . . . . . . . . . . 13 (⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ → (𝑋 ∈ V ∧ 𝑌 ∈ V))
3433adantr 472 . . . . . . . . . . . 12 ((⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑) → (𝑋 ∈ V ∧ 𝑌 ∈ V))
3534exlimivv 2027 . . . . . . . . . . 11 (∃𝑥𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑) → (𝑋 ∈ V ∧ 𝑌 ∈ V))
3635anim1i 608 . . . . . . . . . 10 ((∃𝑥𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑) ∧ 𝑍 ∈ V) → ((𝑋 ∈ V ∧ 𝑌 ∈ V) ∧ 𝑍 ∈ V))
37 df-3an 1109 . . . . . . . . . 10 ((𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V) ↔ ((𝑋 ∈ V ∧ 𝑌 ∈ V) ∧ 𝑍 ∈ V))
3836, 37sylibr 225 . . . . . . . . 9 ((∃𝑥𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑) ∧ 𝑍 ∈ V) → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V))
3938expcom 402 . . . . . . . 8 (𝑍 ∈ V → (∃𝑥𝑦(⟨𝑋, 𝑌⟩ = ⟨𝑥, 𝑦⟩ ∧ [𝑍 / 𝑧]𝜑) → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)))
4024, 39sylbid 231 . . . . . . 7 (𝑍 ∈ V → (⟨⟨𝑋, 𝑌⟩, 𝑍⟩ ∈ {⟨𝑤, 𝑧⟩ ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)))
4140com12 32 . . . . . 6 (⟨⟨𝑋, 𝑌⟩, 𝑍⟩ ∈ {⟨𝑤, 𝑧⟩ ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} → (𝑍 ∈ V → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)))
42 dfoprab2 6903 . . . . . 6 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {⟨𝑤, 𝑧⟩ ∣ ∃𝑥𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
4341, 42eleq2s 2862 . . . . 5 (⟨⟨𝑋, 𝑌⟩, 𝑍⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} → (𝑍 ∈ V → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)))
443, 43sylbi 208 . . . 4 (⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍 → (𝑍 ∈ V → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)))
4544com12 32 . . 3 (𝑍 ∈ V → (⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍 → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)))
4645adantl 473 . 2 ((⟨𝑋, 𝑌⟩ ∈ V ∧ 𝑍 ∈ V) → (⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍 → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V)))
472, 46mpcom 38 1 (⟨𝑋, 𝑌⟩{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}𝑍 → (𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wex 1874  wcel 2155  Vcvv 3350  [wsbc 3598  cop 4342   class class class wbr 4811  {copab 4873  {coprab 6847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pr 5064
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3599  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-if 4246  df-sn 4337  df-pr 4339  df-op 4343  df-br 4812  df-opab 4874  df-xp 5285  df-rel 5286  df-oprab 6850
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator