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

Theorem dmopab2rex 5750
Description: The domain of an ordered pair class abstraction with two nested restricted existential quantifiers. (Contributed by AV, 23-Oct-2023.)
Assertion
Ref Expression
dmopab2rex (∀𝑢𝑈 (∀𝑣𝑉 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝑈 (∃𝑣𝑉 (𝑥 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷))} = {𝑥 ∣ ∃𝑢𝑈 (∃𝑣𝑉 𝑥 = 𝐴 ∨ ∃𝑖𝐼 𝑥 = 𝐶)})
Distinct variable groups:   𝑥,𝐴,𝑦   𝐵,𝑖,𝑥,𝑦   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝐼,𝑦   𝑈,𝑖,𝑥,𝑦   𝑖,𝑉,𝑥,𝑦   𝑖,𝑋   𝑢,𝑖,𝑥,𝑦   𝑣,𝑖,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑣,𝑢,𝑖)   𝐵(𝑣,𝑢)   𝐶(𝑣,𝑢,𝑖)   𝐷(𝑣,𝑢,𝑖)   𝑈(𝑣,𝑢)   𝐼(𝑣,𝑢,𝑖)   𝑉(𝑣,𝑢)   𝑊(𝑥,𝑦,𝑣,𝑢,𝑖)   𝑋(𝑥,𝑦,𝑣,𝑢)

Proof of Theorem dmopab2rex
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 rexcom4 3212 . . . . . . . 8 (∃𝑣𝑉𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑦𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵))
2 rexcom4 3212 . . . . . . . 8 (∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷) ↔ ∃𝑦𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷))
31, 2orbi12i 912 . . . . . . 7 ((∃𝑣𝑉𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ↔ (∃𝑦𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑦𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
4 19.43 1883 . . . . . . 7 (∃𝑦(∃𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)) ↔ (∃𝑦𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑦𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
53, 4bitr4i 281 . . . . . 6 ((∃𝑣𝑉𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ↔ ∃𝑦(∃𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
65rexbii 3210 . . . . 5 (∃𝑢𝑈 (∃𝑣𝑉𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ↔ ∃𝑢𝑈𝑦(∃𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
7 rexcom4 3212 . . . . 5 (∃𝑢𝑈𝑦(∃𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)) ↔ ∃𝑦𝑢𝑈 (∃𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
86, 7bitri 278 . . . 4 (∃𝑢𝑈 (∃𝑣𝑉𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ↔ ∃𝑦𝑢𝑈 (∃𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
9 simpl 486 . . . . . . . . . 10 ((𝑧 = 𝐴𝑦 = 𝐵) → 𝑧 = 𝐴)
109exlimiv 1931 . . . . . . . . 9 (∃𝑦(𝑧 = 𝐴𝑦 = 𝐵) → 𝑧 = 𝐴)
11 elisset 3452 . . . . . . . . . 10 (𝐵𝑋 → ∃𝑦 𝑦 = 𝐵)
12 ibar 532 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (𝑦 = 𝐵 ↔ (𝑧 = 𝐴𝑦 = 𝐵)))
1312bicomd 226 . . . . . . . . . . 11 (𝑧 = 𝐴 → ((𝑧 = 𝐴𝑦 = 𝐵) ↔ 𝑦 = 𝐵))
1413exbidv 1922 . . . . . . . . . 10 (𝑧 = 𝐴 → (∃𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑦 𝑦 = 𝐵))
1511, 14syl5ibrcom 250 . . . . . . . . 9 (𝐵𝑋 → (𝑧 = 𝐴 → ∃𝑦(𝑧 = 𝐴𝑦 = 𝐵)))
1610, 15impbid2 229 . . . . . . . 8 (𝐵𝑋 → (∃𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ 𝑧 = 𝐴))
1716ralrexbid 3281 . . . . . . 7 (∀𝑣𝑉 𝐵𝑋 → (∃𝑣𝑉𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑣𝑉 𝑧 = 𝐴))
1817adantr 484 . . . . . 6 ((∀𝑣𝑉 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → (∃𝑣𝑉𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑣𝑉 𝑧 = 𝐴))
19 simpl 486 . . . . . . . . . 10 ((𝑧 = 𝐶𝑦 = 𝐷) → 𝑧 = 𝐶)
2019exlimiv 1931 . . . . . . . . 9 (∃𝑦(𝑧 = 𝐶𝑦 = 𝐷) → 𝑧 = 𝐶)
21 elisset 3452 . . . . . . . . . 10 (𝐷𝑊 → ∃𝑦 𝑦 = 𝐷)
22 ibar 532 . . . . . . . . . . . 12 (𝑧 = 𝐶 → (𝑦 = 𝐷 ↔ (𝑧 = 𝐶𝑦 = 𝐷)))
2322bicomd 226 . . . . . . . . . . 11 (𝑧 = 𝐶 → ((𝑧 = 𝐶𝑦 = 𝐷) ↔ 𝑦 = 𝐷))
2423exbidv 1922 . . . . . . . . . 10 (𝑧 = 𝐶 → (∃𝑦(𝑧 = 𝐶𝑦 = 𝐷) ↔ ∃𝑦 𝑦 = 𝐷))
2521, 24syl5ibrcom 250 . . . . . . . . 9 (𝐷𝑊 → (𝑧 = 𝐶 → ∃𝑦(𝑧 = 𝐶𝑦 = 𝐷)))
2620, 25impbid2 229 . . . . . . . 8 (𝐷𝑊 → (∃𝑦(𝑧 = 𝐶𝑦 = 𝐷) ↔ 𝑧 = 𝐶))
2726ralrexbid 3281 . . . . . . 7 (∀𝑖𝐼 𝐷𝑊 → (∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷) ↔ ∃𝑖𝐼 𝑧 = 𝐶))
2827adantl 485 . . . . . 6 ((∀𝑣𝑉 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → (∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷) ↔ ∃𝑖𝐼 𝑧 = 𝐶))
2918, 28orbi12d 916 . . . . 5 ((∀𝑣𝑉 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → ((∃𝑣𝑉𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ↔ (∃𝑣𝑉 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶)))
3029ralrexbid 3281 . . . 4 (∀𝑢𝑈 (∀𝑣𝑉 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → (∃𝑢𝑈 (∃𝑣𝑉𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ↔ ∃𝑢𝑈 (∃𝑣𝑉 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶)))
318, 30bitr3id 288 . . 3 (∀𝑢𝑈 (∀𝑣𝑉 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → (∃𝑦𝑢𝑈 (∃𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)) ↔ ∃𝑢𝑈 (∃𝑣𝑉 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶)))
32 eqeq1 2802 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥 = 𝐴𝑧 = 𝐴))
3332anbi1d 632 . . . . . . . 8 (𝑥 = 𝑧 → ((𝑥 = 𝐴𝑦 = 𝐵) ↔ (𝑧 = 𝐴𝑦 = 𝐵)))
3433rexbidv 3256 . . . . . . 7 (𝑥 = 𝑧 → (∃𝑣𝑉 (𝑥 = 𝐴𝑦 = 𝐵) ↔ ∃𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵)))
35 eqeq1 2802 . . . . . . . . 9 (𝑥 = 𝑧 → (𝑥 = 𝐶𝑧 = 𝐶))
3635anbi1d 632 . . . . . . . 8 (𝑥 = 𝑧 → ((𝑥 = 𝐶𝑦 = 𝐷) ↔ (𝑧 = 𝐶𝑦 = 𝐷)))
3736rexbidv 3256 . . . . . . 7 (𝑥 = 𝑧 → (∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷) ↔ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
3834, 37orbi12d 916 . . . . . 6 (𝑥 = 𝑧 → ((∃𝑣𝑉 (𝑥 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷)) ↔ (∃𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷))))
3938rexbidv 3256 . . . . 5 (𝑥 = 𝑧 → (∃𝑢𝑈 (∃𝑣𝑉 (𝑥 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷)) ↔ ∃𝑢𝑈 (∃𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷))))
4039dmopabelb 5749 . . . 4 (𝑧 ∈ V → (𝑧 ∈ dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝑈 (∃𝑣𝑉 (𝑥 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷))} ↔ ∃𝑦𝑢𝑈 (∃𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷))))
4140elv 3446 . . 3 (𝑧 ∈ dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝑈 (∃𝑣𝑉 (𝑥 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷))} ↔ ∃𝑦𝑢𝑈 (∃𝑣𝑉 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
42 vex 3444 . . . 4 𝑧 ∈ V
4332rexbidv 3256 . . . . . 6 (𝑥 = 𝑧 → (∃𝑣𝑉 𝑥 = 𝐴 ↔ ∃𝑣𝑉 𝑧 = 𝐴))
4435rexbidv 3256 . . . . . 6 (𝑥 = 𝑧 → (∃𝑖𝐼 𝑥 = 𝐶 ↔ ∃𝑖𝐼 𝑧 = 𝐶))
4543, 44orbi12d 916 . . . . 5 (𝑥 = 𝑧 → ((∃𝑣𝑉 𝑥 = 𝐴 ∨ ∃𝑖𝐼 𝑥 = 𝐶) ↔ (∃𝑣𝑉 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶)))
4645rexbidv 3256 . . . 4 (𝑥 = 𝑧 → (∃𝑢𝑈 (∃𝑣𝑉 𝑥 = 𝐴 ∨ ∃𝑖𝐼 𝑥 = 𝐶) ↔ ∃𝑢𝑈 (∃𝑣𝑉 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶)))
4742, 46elab 3615 . . 3 (𝑧 ∈ {𝑥 ∣ ∃𝑢𝑈 (∃𝑣𝑉 𝑥 = 𝐴 ∨ ∃𝑖𝐼 𝑥 = 𝐶)} ↔ ∃𝑢𝑈 (∃𝑣𝑉 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶))
4831, 41, 473bitr4g 317 . 2 (∀𝑢𝑈 (∀𝑣𝑉 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → (𝑧 ∈ dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝑈 (∃𝑣𝑉 (𝑥 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷))} ↔ 𝑧 ∈ {𝑥 ∣ ∃𝑢𝑈 (∃𝑣𝑉 𝑥 = 𝐴 ∨ ∃𝑖𝐼 𝑥 = 𝐶)}))
4948eqrdv 2796 1 (∀𝑢𝑈 (∀𝑣𝑉 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → dom {⟨𝑥, 𝑦⟩ ∣ ∃𝑢𝑈 (∃𝑣𝑉 (𝑥 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷))} = {𝑥 ∣ ∃𝑢𝑈 (∃𝑣𝑉 𝑥 = 𝐴 ∨ ∃𝑖𝐼 𝑥 = 𝐶)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wo 844   = wceq 1538  wex 1781  wcel 2111  {cab 2776  wral 3106  wrex 3107  Vcvv 3441  {copab 5092  dom cdm 5519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-dm 5529
This theorem is referenced by:  satffunlem1lem2  32760
  Copyright terms: Public domain W3C validator