Metamath Proof Explorer

Theorem dmopab2rex

Description: The domain of an ordered pair class abstraction with two nested restricted existential quantifiers. (Contributed by AV, 23-Oct-2023)

Ref Expression
Assertion dmopab2rex ( ∀ 𝑢 ∈ 𝑈 ( ∀ 𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 𝐷 ∈ 𝑊 ) → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) } = { 𝑥 ∣ ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝐶 ) } )

Proof

Step Hyp Ref Expression
1 rexcom4 ⊢ ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑦 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ∃ 𝑦 ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) )
2 rexcom4 ⊢ ( ∃ 𝑖 ∈ 𝐼 ∃ 𝑦 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ↔ ∃ 𝑦 ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) )
3 1 2 orbi12i ⊢ ( ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑦 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ∃ 𝑦 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ↔ ( ∃ 𝑦 ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑦 ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) )
4 19.43 ⊢ ( ∃ 𝑦 ( ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ↔ ( ∃ 𝑦 ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑦 ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) )
5 3 4 bitr4i ⊢ ( ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑦 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ∃ 𝑦 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ↔ ∃ 𝑦 ( ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) )
6 5 rexbii ⊢ ( ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑦 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ∃ 𝑦 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ↔ ∃ 𝑢 ∈ 𝑈 ∃ 𝑦 ( ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) )
7 rexcom4 ⊢ ( ∃ 𝑢 ∈ 𝑈 ∃ 𝑦 ( ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ↔ ∃ 𝑦 ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) )
8 6 7 bitri ⊢ ( ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑦 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ∃ 𝑦 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ↔ ∃ 𝑦 ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) )
9 simpl ⊢ ( ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑧 = 𝐴 )
10 9 exlimiv ⊢ ( ∃ 𝑦 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑧 = 𝐴 )
11 elisset ⊢ ( 𝐵 ∈ 𝑋 → ∃ 𝑦 𝑦 = 𝐵 )
12 ibar ⊢ ( 𝑧 = 𝐴 → ( 𝑦 = 𝐵 ↔ ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ) )
13 12 bicomd ⊢ ( 𝑧 = 𝐴 → ( ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ 𝑦 = 𝐵 ) )
14 13 exbidv ⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑦 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ∃ 𝑦 𝑦 = 𝐵 ) )
15 11 14 syl5ibrcom ⊢ ( 𝐵 ∈ 𝑋 → ( 𝑧 = 𝐴 → ∃ 𝑦 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ) )
16 10 15 impbid2 ⊢ ( 𝐵 ∈ 𝑋 → ( ∃ 𝑦 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ 𝑧 = 𝐴 ) )
17 16 ralrexbid ⊢ ( ∀ 𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 → ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑦 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ∃ 𝑣 ∈ 𝑉 𝑧 = 𝐴 ) )
18 17 adantr ⊢ ( ( ∀ 𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 𝐷 ∈ 𝑊 ) → ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑦 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ∃ 𝑣 ∈ 𝑉 𝑧 = 𝐴 ) )
19 simpl ⊢ ( ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) → 𝑧 = 𝐶 )
20 19 exlimiv ⊢ ( ∃ 𝑦 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) → 𝑧 = 𝐶 )
21 elisset ⊢ ( 𝐷 ∈ 𝑊 → ∃ 𝑦 𝑦 = 𝐷 )
22 ibar ⊢ ( 𝑧 = 𝐶 → ( 𝑦 = 𝐷 ↔ ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) )
23 22 bicomd ⊢ ( 𝑧 = 𝐶 → ( ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ↔ 𝑦 = 𝐷 ) )
24 23 exbidv ⊢ ( 𝑧 = 𝐶 → ( ∃ 𝑦 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ↔ ∃ 𝑦 𝑦 = 𝐷 ) )
25 21 24 syl5ibrcom ⊢ ( 𝐷 ∈ 𝑊 → ( 𝑧 = 𝐶 → ∃ 𝑦 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) )
26 20 25 impbid2 ⊢ ( 𝐷 ∈ 𝑊 → ( ∃ 𝑦 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ↔ 𝑧 = 𝐶 ) )
27 26 ralrexbid ⊢ ( ∀ 𝑖 ∈ 𝐼 𝐷 ∈ 𝑊 → ( ∃ 𝑖 ∈ 𝐼 ∃ 𝑦 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑧 = 𝐶 ) )
28 27 adantl ⊢ ( ( ∀ 𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 𝐷 ∈ 𝑊 ) → ( ∃ 𝑖 ∈ 𝐼 ∃ 𝑦 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ↔ ∃ 𝑖 ∈ 𝐼 𝑧 = 𝐶 ) )
29 18 28 orbi12d ⊢ ( ( ∀ 𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 𝐷 ∈ 𝑊 ) → ( ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑦 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ∃ 𝑦 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ↔ ( ∃ 𝑣 ∈ 𝑉 𝑧 = 𝐴 ∨ ∃ 𝑖 ∈ 𝐼 𝑧 = 𝐶 ) ) )
30 29 ralrexbid ⊢ ( ∀ 𝑢 ∈ 𝑈 ( ∀ 𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 𝐷 ∈ 𝑊 ) → ( ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑦 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ∃ 𝑦 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ↔ ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 𝑧 = 𝐴 ∨ ∃ 𝑖 ∈ 𝐼 𝑧 = 𝐶 ) ) )
31 8 30 bitr3id ⊢ ( ∀ 𝑢 ∈ 𝑈 ( ∀ 𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 𝐷 ∈ 𝑊 ) → ( ∃ 𝑦 ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ↔ ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 𝑧 = 𝐴 ∨ ∃ 𝑖 ∈ 𝐼 𝑧 = 𝐶 ) ) )
32 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝐴 ↔ 𝑧 = 𝐴 ) )
33 32 anbi1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ) )
34 33 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑣 ∈ 𝑉 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ) )
35 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = 𝐶 ↔ 𝑧 = 𝐶 ) )
36 35 anbi1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ↔ ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) )
37 36 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑖 ∈ 𝐼 ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ↔ ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) )
38 34 37 orbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ∃ 𝑣 ∈ 𝑉 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ↔ ( ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ) )
39 38 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ↔ ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ) )
40 39 dmopabelb ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) } ↔ ∃ 𝑦 ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ) )
41 40 elv ⊢ ( 𝑧 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) } ↔ ∃ 𝑦 ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ( 𝑧 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑧 = 𝐶 ∧ 𝑦 = 𝐷 ) ) )
42 vex ⊢ 𝑧 ∈ V
43 32 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑣 ∈ 𝑉 𝑥 = 𝐴 ↔ ∃ 𝑣 ∈ 𝑉 𝑧 = 𝐴 ) )
44 35 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑖 ∈ 𝐼 𝑥 = 𝐶 ↔ ∃ 𝑖 ∈ 𝐼 𝑧 = 𝐶 ) )
45 43 44 orbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ∃ 𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝐶 ) ↔ ( ∃ 𝑣 ∈ 𝑉 𝑧 = 𝐴 ∨ ∃ 𝑖 ∈ 𝐼 𝑧 = 𝐶 ) ) )
46 45 rexbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝐶 ) ↔ ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 𝑧 = 𝐴 ∨ ∃ 𝑖 ∈ 𝐼 𝑧 = 𝐶 ) ) )
47 42 46 elab ⊢ ( 𝑧 ∈ { 𝑥 ∣ ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝐶 ) } ↔ ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 𝑧 = 𝐴 ∨ ∃ 𝑖 ∈ 𝐼 𝑧 = 𝐶 ) )
48 31 41 47 3bitr4g ⊢ ( ∀ 𝑢 ∈ 𝑈 ( ∀ 𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 𝐷 ∈ 𝑊 ) → ( 𝑧 ∈ dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) } ↔ 𝑧 ∈ { 𝑥 ∣ ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝐶 ) } ) )
49 48 eqrdv ⊢ ( ∀ 𝑢 ∈ 𝑈 ( ∀ 𝑣 ∈ 𝑉 𝐵 ∈ 𝑋 ∧ ∀ 𝑖 ∈ 𝐼 𝐷 ∈ 𝑊 ) → dom { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∨ ∃ 𝑖 ∈ 𝐼 ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) } = { 𝑥 ∣ ∃ 𝑢 ∈ 𝑈 ( ∃ 𝑣 ∈ 𝑉 𝑥 = 𝐴 ∨ ∃ 𝑖 ∈ 𝐼 𝑥 = 𝐶 ) } )