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 { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢𝑈 ( ∃ 𝑣𝑉 ( 𝑥 = 𝐴𝑦 = 𝐵 ) ∨ ∃ 𝑖𝐼 ( 𝑥 = 𝐶𝑦 = 𝐷 ) ) } = { 𝑥 ∣ ∃ 𝑢𝑈 ( ∃ 𝑣𝑉 𝑥 = 𝐴 ∨ ∃ 𝑖𝐼 𝑥 = 𝐶 ) } )