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∈VB∈X∧∀i∈ID∈W→dom⁡xy|∃u∈U∃v∈Vx=A∧y=B∨∃i∈Ix=C∧y=D=x|∃u∈U∃v∈Vx=A∨∃i∈Ix=C

Proof

Step Hyp Ref Expression
1 rexcom4 ⊢∃v∈V∃yz=A∧y=B↔∃y∃v∈Vz=A∧y=B
2 rexcom4 ⊢∃i∈I∃yz=C∧y=D↔∃y∃i∈Iz=C∧y=D
3 1 2 orbi12i ⊢∃v∈V∃yz=A∧y=B∨∃i∈I∃yz=C∧y=D↔∃y∃v∈Vz=A∧y=B∨∃y∃i∈Iz=C∧y=D
4 19.43 ⊢∃y∃v∈Vz=A∧y=B∨∃i∈Iz=C∧y=D↔∃y∃v∈Vz=A∧y=B∨∃y∃i∈Iz=C∧y=D
5 3 4 bitr4i ⊢∃v∈V∃yz=A∧y=B∨∃i∈I∃yz=C∧y=D↔∃y∃v∈Vz=A∧y=B∨∃i∈Iz=C∧y=D
6 5 rexbii ⊢∃u∈U∃v∈V∃yz=A∧y=B∨∃i∈I∃yz=C∧y=D↔∃u∈U∃y∃v∈Vz=A∧y=B∨∃i∈Iz=C∧y=D
7 rexcom4 ⊢∃u∈U∃y∃v∈Vz=A∧y=B∨∃i∈Iz=C∧y=D↔∃y∃u∈U∃v∈Vz=A∧y=B∨∃i∈Iz=C∧y=D
8 6 7 bitri ⊢∃u∈U∃v∈V∃yz=A∧y=B∨∃i∈I∃yz=C∧y=D↔∃y∃u∈U∃v∈Vz=A∧y=B∨∃i∈Iz=C∧y=D
9 simpl ⊢z=A∧y=B→z=A
10 9 exlimiv ⊢∃yz=A∧y=B→z=A
11 elisset ⊢B∈X→∃yy=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→∃yz=A∧y=B↔∃yy=B
15 11 14 syl5ibrcom ⊢B∈X→z=A→∃yz=A∧y=B
16 10 15 impbid2 ⊢B∈X→∃yz=A∧y=B↔z=A
17 16 ralrexbid ⊢∀v∈VB∈X→∃v∈V∃yz=A∧y=B↔∃v∈Vz=A
18 17 adantr ⊢∀v∈VB∈X∧∀i∈ID∈W→∃v∈V∃yz=A∧y=B↔∃v∈Vz=A
19 simpl ⊢z=C∧y=D→z=C
20 19 exlimiv ⊢∃yz=C∧y=D→z=C
21 elisset ⊢D∈W→∃yy=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→∃yz=C∧y=D↔∃yy=D
25 21 24 syl5ibrcom ⊢D∈W→z=C→∃yz=C∧y=D
26 20 25 impbid2 ⊢D∈W→∃yz=C∧y=D↔z=C
27 26 ralrexbid ⊢∀i∈ID∈W→∃i∈I∃yz=C∧y=D↔∃i∈Iz=C
28 27 adantl ⊢∀v∈VB∈X∧∀i∈ID∈W→∃i∈I∃yz=C∧y=D↔∃i∈Iz=C
29 18 28 orbi12d ⊢∀v∈VB∈X∧∀i∈ID∈W→∃v∈V∃yz=A∧y=B∨∃i∈I∃yz=C∧y=D↔∃v∈Vz=A∨∃i∈Iz=C
30 29 ralrexbid ⊢∀u∈U∀v∈VB∈X∧∀i∈ID∈W→∃u∈U∃v∈V∃yz=A∧y=B∨∃i∈I∃yz=C∧y=D↔∃u∈U∃v∈Vz=A∨∃i∈Iz=C
31 8 30 bitr3id ⊢∀u∈U∀v∈VB∈X∧∀i∈ID∈W→∃y∃u∈U∃v∈Vz=A∧y=B∨∃i∈Iz=C∧y=D↔∃u∈U∃v∈Vz=A∨∃i∈Iz=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∈Vx=A∧y=B↔∃v∈Vz=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∈Ix=C∧y=D↔∃i∈Iz=C∧y=D
38 34 37 orbi12d ⊢x=z→∃v∈Vx=A∧y=B∨∃i∈Ix=C∧y=D↔∃v∈Vz=A∧y=B∨∃i∈Iz=C∧y=D
39 38 rexbidv ⊢x=z→∃u∈U∃v∈Vx=A∧y=B∨∃i∈Ix=C∧y=D↔∃u∈U∃v∈Vz=A∧y=B∨∃i∈Iz=C∧y=D
40 39 dmopabelb ⊢z∈V→z∈dom⁡xy|∃u∈U∃v∈Vx=A∧y=B∨∃i∈Ix=C∧y=D↔∃y∃u∈U∃v∈Vz=A∧y=B∨∃i∈Iz=C∧y=D
41 40 elv ⊢z∈dom⁡xy|∃u∈U∃v∈Vx=A∧y=B∨∃i∈Ix=C∧y=D↔∃y∃u∈U∃v∈Vz=A∧y=B∨∃i∈Iz=C∧y=D
42 vex ⊢z∈V
43 32 rexbidv ⊢x=z→∃v∈Vx=A↔∃v∈Vz=A
44 35 rexbidv ⊢x=z→∃i∈Ix=C↔∃i∈Iz=C
45 43 44 orbi12d ⊢x=z→∃v∈Vx=A∨∃i∈Ix=C↔∃v∈Vz=A∨∃i∈Iz=C
46 45 rexbidv ⊢x=z→∃u∈U∃v∈Vx=A∨∃i∈Ix=C↔∃u∈U∃v∈Vz=A∨∃i∈Iz=C
47 42 46 elab ⊢z∈x|∃u∈U∃v∈Vx=A∨∃i∈Ix=C↔∃u∈U∃v∈Vz=A∨∃i∈Iz=C
48 31 41 47 3bitr4g ⊢∀u∈U∀v∈VB∈X∧∀i∈ID∈W→z∈dom⁡xy|∃u∈U∃v∈Vx=A∧y=B∨∃i∈Ix=C∧y=D↔z∈x|∃u∈U∃v∈Vx=A∨∃i∈Ix=C
49 48 eqrdv ⊢∀u∈U∀v∈VB∈X∧∀i∈ID∈W→dom⁡xy|∃u∈U∃v∈Vx=A∧y=B∨∃i∈Ix=C∧y=D=x|∃u∈U∃v∈Vx=A∨∃i∈Ix=C