Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dmopab3rexdif Structured version   Visualization version   GIF version

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

Proof of Theorem dmopab3rexdif
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 rexcom4 3212 . . . . . . . . . 10 (∃𝑣𝑈𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑦𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵))
2 rexcom4 3212 . . . . . . . . . 10 (∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷) ↔ ∃𝑦𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷))
31, 2orbi12i 912 . . . . . . . . 9 ((∃𝑣𝑈𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ↔ (∃𝑦𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑦𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
4 19.43 1883 . . . . . . . . 9 (∃𝑦(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)) ↔ (∃𝑦𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑦𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
53, 4bitr4i 281 . . . . . . . 8 ((∃𝑣𝑈𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ↔ ∃𝑦(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
65rexbii 3210 . . . . . . 7 (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ↔ ∃𝑢 ∈ (𝑈𝑆)∃𝑦(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
7 rexcom4 3212 . . . . . . 7 (∃𝑢 ∈ (𝑈𝑆)∃𝑦(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)) ↔ ∃𝑦𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
86, 7bitri 278 . . . . . 6 (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ↔ ∃𝑦𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
9 rexcom4 3212 . . . . . . . 8 (∃𝑣 ∈ (𝑈𝑆)∃𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑦𝑣 ∈ (𝑈𝑆)(𝑧 = 𝐴𝑦 = 𝐵))
109rexbii 3210 . . . . . . 7 (∃𝑢𝑆𝑣 ∈ (𝑈𝑆)∃𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑢𝑆𝑦𝑣 ∈ (𝑈𝑆)(𝑧 = 𝐴𝑦 = 𝐵))
11 rexcom4 3212 . . . . . . 7 (∃𝑢𝑆𝑦𝑣 ∈ (𝑈𝑆)(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑦𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑧 = 𝐴𝑦 = 𝐵))
1210, 11bitri 278 . . . . . 6 (∃𝑢𝑆𝑣 ∈ (𝑈𝑆)∃𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑦𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑧 = 𝐴𝑦 = 𝐵))
138, 12orbi12i 912 . . . . 5 ((∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)∃𝑦(𝑧 = 𝐴𝑦 = 𝐵)) ↔ (∃𝑦𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑦𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑧 = 𝐴𝑦 = 𝐵)))
14 19.43 1883 . . . . 5 (∃𝑦(∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑧 = 𝐴𝑦 = 𝐵)) ↔ (∃𝑦𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑦𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑧 = 𝐴𝑦 = 𝐵)))
1513, 14bitr4i 281 . . . 4 ((∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)∃𝑦(𝑧 = 𝐴𝑦 = 𝐵)) ↔ ∃𝑦(∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑧 = 𝐴𝑦 = 𝐵)))
16 difssd 4062 . . . . . . . 8 (𝑆𝑈 → (𝑈𝑆) ⊆ 𝑈)
17 ssralv 3982 . . . . . . . 8 ((𝑈𝑆) ⊆ 𝑈 → (∀𝑢𝑈 (∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → ∀𝑢 ∈ (𝑈𝑆)(∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊)))
1816, 17syl 17 . . . . . . 7 (𝑆𝑈 → (∀𝑢𝑈 (∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → ∀𝑢 ∈ (𝑈𝑆)(∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊)))
1918impcom 411 . . . . . 6 ((∀𝑢𝑈 (∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) ∧ 𝑆𝑈) → ∀𝑢 ∈ (𝑈𝑆)(∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊))
20 simpl 486 . . . . . . . . . . . 12 ((𝑧 = 𝐴𝑦 = 𝐵) → 𝑧 = 𝐴)
2120exlimiv 1931 . . . . . . . . . . 11 (∃𝑦(𝑧 = 𝐴𝑦 = 𝐵) → 𝑧 = 𝐴)
22 elisset 3452 . . . . . . . . . . . 12 (𝐵𝑋 → ∃𝑦 𝑦 = 𝐵)
23 ibar 532 . . . . . . . . . . . . . 14 (𝑧 = 𝐴 → (𝑦 = 𝐵 ↔ (𝑧 = 𝐴𝑦 = 𝐵)))
2423bicomd 226 . . . . . . . . . . . . 13 (𝑧 = 𝐴 → ((𝑧 = 𝐴𝑦 = 𝐵) ↔ 𝑦 = 𝐵))
2524exbidv 1922 . . . . . . . . . . . 12 (𝑧 = 𝐴 → (∃𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑦 𝑦 = 𝐵))
2622, 25syl5ibrcom 250 . . . . . . . . . . 11 (𝐵𝑋 → (𝑧 = 𝐴 → ∃𝑦(𝑧 = 𝐴𝑦 = 𝐵)))
2721, 26impbid2 229 . . . . . . . . . 10 (𝐵𝑋 → (∃𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ 𝑧 = 𝐴))
2827ralrexbid 3281 . . . . . . . . 9 (∀𝑣𝑈 𝐵𝑋 → (∃𝑣𝑈𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑣𝑈 𝑧 = 𝐴))
2928adantr 484 . . . . . . . 8 ((∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → (∃𝑣𝑈𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑣𝑈 𝑧 = 𝐴))
30 simpl 486 . . . . . . . . . . . 12 ((𝑧 = 𝐶𝑦 = 𝐷) → 𝑧 = 𝐶)
3130exlimiv 1931 . . . . . . . . . . 11 (∃𝑦(𝑧 = 𝐶𝑦 = 𝐷) → 𝑧 = 𝐶)
32 elisset 3452 . . . . . . . . . . . 12 (𝐷𝑊 → ∃𝑦 𝑦 = 𝐷)
33 ibar 532 . . . . . . . . . . . . . 14 (𝑧 = 𝐶 → (𝑦 = 𝐷 ↔ (𝑧 = 𝐶𝑦 = 𝐷)))
3433bicomd 226 . . . . . . . . . . . . 13 (𝑧 = 𝐶 → ((𝑧 = 𝐶𝑦 = 𝐷) ↔ 𝑦 = 𝐷))
3534exbidv 1922 . . . . . . . . . . . 12 (𝑧 = 𝐶 → (∃𝑦(𝑧 = 𝐶𝑦 = 𝐷) ↔ ∃𝑦 𝑦 = 𝐷))
3632, 35syl5ibrcom 250 . . . . . . . . . . 11 (𝐷𝑊 → (𝑧 = 𝐶 → ∃𝑦(𝑧 = 𝐶𝑦 = 𝐷)))
3731, 36impbid2 229 . . . . . . . . . 10 (𝐷𝑊 → (∃𝑦(𝑧 = 𝐶𝑦 = 𝐷) ↔ 𝑧 = 𝐶))
3837ralrexbid 3281 . . . . . . . . 9 (∀𝑖𝐼 𝐷𝑊 → (∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷) ↔ ∃𝑖𝐼 𝑧 = 𝐶))
3938adantl 485 . . . . . . . 8 ((∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → (∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷) ↔ ∃𝑖𝐼 𝑧 = 𝐶))
4029, 39orbi12d 916 . . . . . . 7 ((∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → ((∃𝑣𝑈𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ↔ (∃𝑣𝑈 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶)))
4140ralrexbid 3281 . . . . . 6 (∀𝑢 ∈ (𝑈𝑆)(∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ↔ ∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶)))
4219, 41syl 17 . . . . 5 ((∀𝑢𝑈 (∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) ∧ 𝑆𝑈) → (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ↔ ∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶)))
43 ssralv 3982 . . . . . . . 8 (𝑆𝑈 → (∀𝑢𝑈 (∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → ∀𝑢𝑆 (∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊)))
44 ssralv 3982 . . . . . . . . . . 11 ((𝑈𝑆) ⊆ 𝑈 → (∀𝑣𝑈 𝐵𝑋 → ∀𝑣 ∈ (𝑈𝑆)𝐵𝑋))
4516, 44syl 17 . . . . . . . . . 10 (𝑆𝑈 → (∀𝑣𝑈 𝐵𝑋 → ∀𝑣 ∈ (𝑈𝑆)𝐵𝑋))
4645adantrd 495 . . . . . . . . 9 (𝑆𝑈 → ((∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → ∀𝑣 ∈ (𝑈𝑆)𝐵𝑋))
4746ralimdv 3145 . . . . . . . 8 (𝑆𝑈 → (∀𝑢𝑆 (∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → ∀𝑢𝑆𝑣 ∈ (𝑈𝑆)𝐵𝑋))
4843, 47syld 47 . . . . . . 7 (𝑆𝑈 → (∀𝑢𝑈 (∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) → ∀𝑢𝑆𝑣 ∈ (𝑈𝑆)𝐵𝑋))
4948impcom 411 . . . . . 6 ((∀𝑢𝑈 (∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) ∧ 𝑆𝑈) → ∀𝑢𝑆𝑣 ∈ (𝑈𝑆)𝐵𝑋)
5027ralrexbid 3281 . . . . . . 7 (∀𝑣 ∈ (𝑈𝑆)𝐵𝑋 → (∃𝑣 ∈ (𝑈𝑆)∃𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑣 ∈ (𝑈𝑆)𝑧 = 𝐴))
5150ralrexbid 3281 . . . . . 6 (∀𝑢𝑆𝑣 ∈ (𝑈𝑆)𝐵𝑋 → (∃𝑢𝑆𝑣 ∈ (𝑈𝑆)∃𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)𝑧 = 𝐴))
5249, 51syl 17 . . . . 5 ((∀𝑢𝑈 (∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) ∧ 𝑆𝑈) → (∃𝑢𝑆𝑣 ∈ (𝑈𝑆)∃𝑦(𝑧 = 𝐴𝑦 = 𝐵) ↔ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)𝑧 = 𝐴))
5342, 52orbi12d 916 . . . 4 ((∀𝑢𝑈 (∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) ∧ 𝑆𝑈) → ((∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈𝑦(𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼𝑦(𝑧 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)∃𝑦(𝑧 = 𝐴𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)𝑧 = 𝐴)))
5415, 53bitr3id 288 . . 3 ((∀𝑢𝑈 (∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) ∧ 𝑆𝑈) → (∃𝑦(∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑧 = 𝐴𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)𝑧 = 𝐴)))
55 eqeq1 2802 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥 = 𝐴𝑧 = 𝐴))
5655anbi1d 632 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝑥 = 𝐴𝑦 = 𝐵) ↔ (𝑧 = 𝐴𝑦 = 𝐵)))
5756rexbidv 3256 . . . . . . . 8 (𝑥 = 𝑧 → (∃𝑣𝑈 (𝑥 = 𝐴𝑦 = 𝐵) ↔ ∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵)))
58 eqeq1 2802 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝑥 = 𝐶𝑧 = 𝐶))
5958anbi1d 632 . . . . . . . . 9 (𝑥 = 𝑧 → ((𝑥 = 𝐶𝑦 = 𝐷) ↔ (𝑧 = 𝐶𝑦 = 𝐷)))
6059rexbidv 3256 . . . . . . . 8 (𝑥 = 𝑧 → (∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷) ↔ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)))
6157, 60orbi12d 916 . . . . . . 7 (𝑥 = 𝑧 → ((∃𝑣𝑈 (𝑥 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷)) ↔ (∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷))))
6261rexbidv 3256 . . . . . 6 (𝑥 = 𝑧 → (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑥 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷)) ↔ ∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷))))
63562rexbidv 3259 . . . . . 6 (𝑥 = 𝑧 → (∃𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑥 = 𝐴𝑦 = 𝐵) ↔ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑧 = 𝐴𝑦 = 𝐵)))
6462, 63orbi12d 916 . . . . 5 (𝑥 = 𝑧 → ((∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑥 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑥 = 𝐴𝑦 = 𝐵)) ↔ (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑧 = 𝐴𝑦 = 𝐵))))
6564dmopabelb 5754 . . . 4 (𝑧 ∈ V → (𝑧 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑥 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑥 = 𝐴𝑦 = 𝐵))} ↔ ∃𝑦(∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑧 = 𝐴𝑦 = 𝐵))))
6665elv 3446 . . 3 (𝑧 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑥 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑥 = 𝐴𝑦 = 𝐵))} ↔ ∃𝑦(∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑧 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑧 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑧 = 𝐴𝑦 = 𝐵)))
67 vex 3444 . . . 4 𝑧 ∈ V
6855rexbidv 3256 . . . . . . 7 (𝑥 = 𝑧 → (∃𝑣𝑈 𝑥 = 𝐴 ↔ ∃𝑣𝑈 𝑧 = 𝐴))
6958rexbidv 3256 . . . . . . 7 (𝑥 = 𝑧 → (∃𝑖𝐼 𝑥 = 𝐶 ↔ ∃𝑖𝐼 𝑧 = 𝐶))
7068, 69orbi12d 916 . . . . . 6 (𝑥 = 𝑧 → ((∃𝑣𝑈 𝑥 = 𝐴 ∨ ∃𝑖𝐼 𝑥 = 𝐶) ↔ (∃𝑣𝑈 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶)))
7170rexbidv 3256 . . . . 5 (𝑥 = 𝑧 → (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 𝑥 = 𝐴 ∨ ∃𝑖𝐼 𝑥 = 𝐶) ↔ ∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶)))
72552rexbidv 3259 . . . . 5 (𝑥 = 𝑧 → (∃𝑢𝑆𝑣 ∈ (𝑈𝑆)𝑥 = 𝐴 ↔ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)𝑧 = 𝐴))
7371, 72orbi12d 916 . . . 4 (𝑥 = 𝑧 → ((∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 𝑥 = 𝐴 ∨ ∃𝑖𝐼 𝑥 = 𝐶) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)𝑥 = 𝐴) ↔ (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)𝑧 = 𝐴)))
7467, 73elab 3615 . . 3 (𝑧 ∈ {𝑥 ∣ (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 𝑥 = 𝐴 ∨ ∃𝑖𝐼 𝑥 = 𝐶) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)𝑥 = 𝐴)} ↔ (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 𝑧 = 𝐴 ∨ ∃𝑖𝐼 𝑧 = 𝐶) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)𝑧 = 𝐴))
7554, 66, 743bitr4g 317 . 2 ((∀𝑢𝑈 (∀𝑣𝑈 𝐵𝑋 ∧ ∀𝑖𝐼 𝐷𝑊) ∧ 𝑆𝑈) → (𝑧 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 (𝑥 = 𝐴𝑦 = 𝐵) ∨ ∃𝑖𝐼 (𝑥 = 𝐶𝑦 = 𝐷)) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)(𝑥 = 𝐴𝑦 = 𝐵))} ↔ 𝑧 ∈ {𝑥 ∣ (∃𝑢 ∈ (𝑈𝑆)(∃𝑣𝑈 𝑥 = 𝐴 ∨ ∃𝑖𝐼 𝑥 = 𝐶) ∨ ∃𝑢𝑆𝑣 ∈ (𝑈𝑆)𝑥 = 𝐴)}))
7675eqrdv 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   ∖ cdif 3879   ⊆ wss 3882  {copab 5095  dom cdm 5522 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 5170  ax-nul 5177  ax-pr 5298 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 3885  df-un 3887  df-in 3889  df-ss 3899  df-nul 4246  df-if 4428  df-sn 4528  df-pr 4530  df-op 4534  df-br 5034  df-opab 5096  df-dm 5532 This theorem is referenced by:  satffunlem2lem2  32829
 Copyright terms: Public domain W3C validator