ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eloprabga GIF version

Theorem eloprabga 5790
Description: The law of concretion for operation class abstraction. Compare elopab 4118. (Contributed by NM, 14-Sep-1999.) (Unnecessary distinct variable restrictions were removed by David Abernethy, 19-Jun-2012.) (Revised by Mario Carneiro, 19-Dec-2013.)
Hypothesis
Ref Expression
eloprabga.1 ((𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶) → (𝜑𝜓))
Assertion
Ref Expression
eloprabga ((𝐴𝑉𝐵𝑊𝐶𝑋) → (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜓))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝜓,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝑉(𝑥,𝑦,𝑧)   𝑊(𝑥,𝑦,𝑧)   𝑋(𝑥,𝑦,𝑧)

Proof of Theorem eloprabga
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 elex 2652 . 2 (𝐴𝑉𝐴 ∈ V)
2 elex 2652 . 2 (𝐵𝑊𝐵 ∈ V)
3 elex 2652 . 2 (𝐶𝑋𝐶 ∈ V)
4 opexg 4088 . . . . 5 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ⟨𝐴, 𝐵⟩ ∈ V)
5 opexg 4088 . . . . 5 ((⟨𝐴, 𝐵⟩ ∈ V ∧ 𝐶 ∈ V) → ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ V)
64, 5sylan 279 . . . 4 (((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝐶 ∈ V) → ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ V)
763impa 1144 . . 3 ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ V)
8 simpr 109 . . . . . . . . . . 11 (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩) → 𝑤 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩)
98eqeq1d 2108 . . . . . . . . . 10 (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
10 eqcom 2102 . . . . . . . . . . 11 (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩)
11 vex 2644 . . . . . . . . . . . 12 𝑥 ∈ V
12 vex 2644 . . . . . . . . . . . 12 𝑦 ∈ V
13 vex 2644 . . . . . . . . . . . 12 𝑧 ∈ V
1411, 12, 13otth2 4101 . . . . . . . . . . 11 (⟨⟨𝑥, 𝑦⟩, 𝑧⟩ = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ↔ (𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶))
1510, 14bitri 183 . . . . . . . . . 10 (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ (𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶))
169, 15syl6bb 195 . . . . . . . . 9 (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩) → (𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ↔ (𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶)))
1716anbi1d 456 . . . . . . . 8 (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩) → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ((𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶) ∧ 𝜑)))
18 eloprabga.1 . . . . . . . . 9 ((𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶) → (𝜑𝜓))
1918pm5.32i 445 . . . . . . . 8 (((𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶) ∧ 𝜑) ↔ ((𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶) ∧ 𝜓))
2017, 19syl6bb 195 . . . . . . 7 (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩) → ((𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ((𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶) ∧ 𝜓)))
21203exbidv 1808 . . . . . 6 (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩) → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ∃𝑥𝑦𝑧((𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶) ∧ 𝜓)))
22 df-oprab 5710 . . . . . . . . . 10 {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} = {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)}
2322eleq2i 2166 . . . . . . . . 9 (𝑤 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝑤 ∈ {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)})
24 abid 2088 . . . . . . . . 9 (𝑤 ∈ {𝑤 ∣ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑)} ↔ ∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑))
2523, 24bitr2i 184 . . . . . . . 8 (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ 𝑤 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑})
26 eleq1 2162 . . . . . . . 8 (𝑤 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ → (𝑤 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}))
2725, 26syl5bb 191 . . . . . . 7 (𝑤 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}))
2827adantl 273 . . . . . 6 (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩) → (∃𝑥𝑦𝑧(𝑤 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∧ 𝜑) ↔ ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑}))
29 elisset 2655 . . . . . . . . . . 11 (𝐴 ∈ V → ∃𝑥 𝑥 = 𝐴)
30 elisset 2655 . . . . . . . . . . 11 (𝐵 ∈ V → ∃𝑦 𝑦 = 𝐵)
31 elisset 2655 . . . . . . . . . . 11 (𝐶 ∈ V → ∃𝑧 𝑧 = 𝐶)
3229, 30, 313anim123i 1134 . . . . . . . . . 10 ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶))
33 eeeanv 1868 . . . . . . . . . 10 (∃𝑥𝑦𝑧(𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵 ∧ ∃𝑧 𝑧 = 𝐶))
3432, 33sylibr 133 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → ∃𝑥𝑦𝑧(𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶))
3534biantrurd 301 . . . . . . . 8 ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (𝜓 ↔ (∃𝑥𝑦𝑧(𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶) ∧ 𝜓)))
36 19.41vvv 1843 . . . . . . . 8 (∃𝑥𝑦𝑧((𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶) ∧ 𝜓) ↔ (∃𝑥𝑦𝑧(𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶) ∧ 𝜓))
3735, 36syl6rbbr 198 . . . . . . 7 ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (∃𝑥𝑦𝑧((𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶) ∧ 𝜓) ↔ 𝜓))
3837adantr 272 . . . . . 6 (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩) → (∃𝑥𝑦𝑧((𝑥 = 𝐴𝑦 = 𝐵𝑧 = 𝐶) ∧ 𝜓) ↔ 𝜓))
3921, 28, 383bitr3d 217 . . . . 5 (((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) ∧ 𝑤 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩) → (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜓))
4039expcom 115 . . . 4 (𝑤 = ⟨⟨𝐴, 𝐵⟩, 𝐶⟩ → ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜓)))
4140vtocleg 2712 . . 3 (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ V → ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜓)))
427, 41mpcom 36 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V) → (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜓))
431, 2, 3, 42syl3an 1226 1 ((𝐴𝑉𝐵𝑊𝐶𝑋) → (⟨⟨𝐴, 𝐵⟩, 𝐶⟩ ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ↔ 𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 930   = wceq 1299  wex 1436  wcel 1448  {cab 2086  Vcvv 2641  cop 3477  {coprab 5707
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069
This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-un 3025  df-in 3027  df-ss 3034  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-oprab 5710
This theorem is referenced by:  eloprabg  5791  ovigg  5823
  Copyright terms: Public domain W3C validator