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 ⊢ ∀ u ∈ U ∀ v ∈ V B ∈ X ∧ ∀ i ∈ I D ∈ W → dom ⁡ x y | ∃ u ∈ U ∃ v ∈ V x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D = x | ∃ u ∈ U ∃ v ∈ V x = A ∨ ∃ i ∈ I x = C

Proof

Step Hyp Ref Expression
1 rexcom4 ⊢ ∃ v ∈ V ∃ y z = A ∧ y = B ↔ ∃ y ∃ v ∈ V z = A ∧ y = B
2 rexcom4 ⊢ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ y ∃ i ∈ I z = C ∧ y = D
3 1 2 orbi12i ⊢ ∃ v ∈ V ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ y ∃ v ∈ V z = A ∧ y = B ∨ ∃ y ∃ i ∈ I z = C ∧ y = D
4 19.43 ⊢ ∃ y ∃ v ∈ V z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D ↔ ∃ y ∃ v ∈ V z = A ∧ y = B ∨ ∃ y ∃ i ∈ I z = C ∧ y = D
5 3 4 bitr4i ⊢ ∃ v ∈ V ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ y ∃ v ∈ V z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D
6 5 rexbii ⊢ ∃ u ∈ U ∃ v ∈ V ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ u ∈ U ∃ y ∃ v ∈ V z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D
7 rexcom4 ⊢ ∃ u ∈ U ∃ y ∃ v ∈ V z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D ↔ ∃ y ∃ u ∈ U ∃ v ∈ V z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D
8 6 7 bitri ⊢ ∃ u ∈ U ∃ v ∈ V ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ y ∃ u ∈ U ∃ v ∈ V z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D
9 simpl ⊢ z = A ∧ y = B → z = A
10 9 exlimiv ⊢ ∃ y z = A ∧ y = B → z = A
11 elisset ⊢ B ∈ X → ∃ y y = B
12 ibar ⊢ z = A → y = B ↔ z = A ∧ y = B
13 12 bicomd ⊢ z = A → z = A ∧ y = B ↔ y = B
14 13 exbidv ⊢ z = A → ∃ y z = A ∧ y = B ↔ ∃ y y = B
15 11 14 syl5ibrcom ⊢ B ∈ X → z = A → ∃ y z = A ∧ y = B
16 10 15 impbid2 ⊢ B ∈ X → ∃ y z = A ∧ y = B ↔ z = A
17 16 ralrexbid ⊢ ∀ v ∈ V B ∈ X → ∃ v ∈ V ∃ y z = A ∧ y = B ↔ ∃ v ∈ V z = A
18 17 adantr ⊢ ∀ v ∈ V B ∈ X ∧ ∀ i ∈ I D ∈ W → ∃ v ∈ V ∃ y z = A ∧ y = B ↔ ∃ v ∈ V z = A
19 simpl ⊢ z = C ∧ y = D → z = C
20 19 exlimiv ⊢ ∃ y z = C ∧ y = D → z = C
21 elisset ⊢ D ∈ W → ∃ y y = D
22 ibar ⊢ z = C → y = D ↔ z = C ∧ y = D
23 22 bicomd ⊢ z = C → z = C ∧ y = D ↔ y = D
24 23 exbidv ⊢ z = C → ∃ y z = C ∧ y = D ↔ ∃ y y = D
25 21 24 syl5ibrcom ⊢ D ∈ W → z = C → ∃ y z = C ∧ y = D
26 20 25 impbid2 ⊢ D ∈ W → ∃ y z = C ∧ y = D ↔ z = C
27 26 ralrexbid ⊢ ∀ i ∈ I D ∈ W → ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ i ∈ I z = C
28 27 adantl ⊢ ∀ v ∈ V B ∈ X ∧ ∀ i ∈ I D ∈ W → ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ i ∈ I z = C
29 18 28 orbi12d ⊢ ∀ v ∈ V B ∈ X ∧ ∀ i ∈ I D ∈ W → ∃ v ∈ V ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ v ∈ V z = A ∨ ∃ i ∈ I z = C
30 29 ralrexbid ⊢ ∀ u ∈ U ∀ v ∈ V B ∈ X ∧ ∀ i ∈ I D ∈ W → ∃ u ∈ U ∃ v ∈ V ∃ y z = A ∧ y = B ∨ ∃ i ∈ I ∃ y z = C ∧ y = D ↔ ∃ u ∈ U ∃ v ∈ V z = A ∨ ∃ i ∈ I z = C
31 8 30 syl5bbr ⊢ ∀ u ∈ U ∀ v ∈ V B ∈ X ∧ ∀ i ∈ I D ∈ W → ∃ y ∃ u ∈ U ∃ v ∈ V z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D ↔ ∃ u ∈ U ∃ v ∈ V z = A ∨ ∃ i ∈ I z = C
32 eqeq1 ⊢ x = z → x = A ↔ z = A
33 32 anbi1d ⊢ x = z → x = A ∧ y = B ↔ z = A ∧ y = B
34 33 rexbidv ⊢ x = z → ∃ v ∈ V x = A ∧ y = B ↔ ∃ v ∈ V z = A ∧ y = B
35 eqeq1 ⊢ x = z → x = C ↔ z = C
36 35 anbi1d ⊢ x = z → x = C ∧ y = D ↔ z = C ∧ y = D
37 36 rexbidv ⊢ x = z → ∃ i ∈ I x = C ∧ y = D ↔ ∃ i ∈ I z = C ∧ y = D
38 34 37 orbi12d ⊢ x = z → ∃ v ∈ V x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D ↔ ∃ v ∈ V z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D
39 38 rexbidv ⊢ x = z → ∃ u ∈ U ∃ v ∈ V x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D ↔ ∃ u ∈ U ∃ v ∈ V z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D
40 39 dmopabelb ⊢ z ∈ V → z ∈ dom ⁡ x y | ∃ u ∈ U ∃ v ∈ V x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D ↔ ∃ y ∃ u ∈ U ∃ v ∈ V z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D
41 40 elv ⊢ z ∈ dom ⁡ x y | ∃ u ∈ U ∃ v ∈ V x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D ↔ ∃ y ∃ u ∈ U ∃ v ∈ V z = A ∧ y = B ∨ ∃ i ∈ I z = C ∧ y = D
42 vex ⊢ z ∈ V
43 32 rexbidv ⊢ x = z → ∃ v ∈ V x = A ↔ ∃ v ∈ V z = A
44 35 rexbidv ⊢ x = z → ∃ i ∈ I x = C ↔ ∃ i ∈ I z = C
45 43 44 orbi12d ⊢ x = z → ∃ v ∈ V x = A ∨ ∃ i ∈ I x = C ↔ ∃ v ∈ V z = A ∨ ∃ i ∈ I z = C
46 45 rexbidv ⊢ x = z → ∃ u ∈ U ∃ v ∈ V x = A ∨ ∃ i ∈ I x = C ↔ ∃ u ∈ U ∃ v ∈ V z = A ∨ ∃ i ∈ I z = C
47 42 46 elab ⊢ z ∈ x | ∃ u ∈ U ∃ v ∈ V x = A ∨ ∃ i ∈ I x = C ↔ ∃ u ∈ U ∃ v ∈ V z = A ∨ ∃ i ∈ I z = C
48 31 41 47 3bitr4g ⊢ ∀ u ∈ U ∀ v ∈ V B ∈ X ∧ ∀ i ∈ I D ∈ W → z ∈ dom ⁡ x y | ∃ u ∈ U ∃ v ∈ V x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D ↔ z ∈ x | ∃ u ∈ U ∃ v ∈ V x = A ∨ ∃ i ∈ I x = C
49 48 eqrdv ⊢ ∀ u ∈ U ∀ v ∈ V B ∈ X ∧ ∀ i ∈ I D ∈ W → dom ⁡ x y | ∃ u ∈ U ∃ v ∈ V x = A ∧ y = B ∨ ∃ i ∈ I x = C ∧ y = D = x | ∃ u ∈ U ∃ v ∈ V x = A ∨ ∃ i ∈ I x = C