This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( A. u e. U ( A. v e. V B e. X /\ A. i e. I D e. W ) -> dom { <. x , y >. | E. u e. U ( E. v e. V ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) } = { x | E. u e. U ( E. v e. V x = A \/ E. i e. I x = C ) } )

Proof

Step Hyp Ref Expression
1 rexcom4 
 |-  ( E. v e. V E. y ( z = A /\ y = B ) <-> E. y E. v e. V ( z = A /\ y = B ) )
2 rexcom4 
 |-  ( E. i e. I E. y ( z = C /\ y = D ) <-> E. y E. i e. I ( z = C /\ y = D ) )
3 1 2 orbi12i 
 |-  ( ( E. v e. V E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) <-> ( E. y E. v e. V ( z = A /\ y = B ) \/ E. y E. i e. I ( z = C /\ y = D ) ) )
4 19.43 
 |-  ( E. y ( E. v e. V ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) <-> ( E. y E. v e. V ( z = A /\ y = B ) \/ E. y E. i e. I ( z = C /\ y = D ) ) )
5 3 4 bitr4i 
 |-  ( ( E. v e. V E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) <-> E. y ( E. v e. V ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) )
6 5 rexbii 
 |-  ( E. u e. U ( E. v e. V E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) <-> E. u e. U E. y ( E. v e. V ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) )
7 rexcom4 
 |-  ( E. u e. U E. y ( E. v e. V ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) <-> E. y E. u e. U ( E. v e. V ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) )
8 6 7 bitri 
 |-  ( E. u e. U ( E. v e. V E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) <-> E. y E. u e. U ( E. v e. V ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) )
9 simpl 
 |-  ( ( z = A /\ y = B ) -> z = A )
10 9 exlimiv 
 |-  ( E. y ( z = A /\ y = B ) -> z = A )
11 elisset 
 |-  ( B e. X -> E. 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 -> ( E. y ( z = A /\ y = B ) <-> E. y y = B ) )
15 11 14 syl5ibrcom 
 |-  ( B e. X -> ( z = A -> E. y ( z = A /\ y = B ) ) )
16 10 15 impbid2 
 |-  ( B e. X -> ( E. y ( z = A /\ y = B ) <-> z = A ) )
17 16 ralrexbid 
 |-  ( A. v e. V B e. X -> ( E. v e. V E. y ( z = A /\ y = B ) <-> E. v e. V z = A ) )
18 17 adantr 
 |-  ( ( A. v e. V B e. X /\ A. i e. I D e. W ) -> ( E. v e. V E. y ( z = A /\ y = B ) <-> E. v e. V z = A ) )
19 simpl 
 |-  ( ( z = C /\ y = D ) -> z = C )
20 19 exlimiv 
 |-  ( E. y ( z = C /\ y = D ) -> z = C )
21 elisset 
 |-  ( D e. W -> E. 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 -> ( E. y ( z = C /\ y = D ) <-> E. y y = D ) )
25 21 24 syl5ibrcom 
 |-  ( D e. W -> ( z = C -> E. y ( z = C /\ y = D ) ) )
26 20 25 impbid2 
 |-  ( D e. W -> ( E. y ( z = C /\ y = D ) <-> z = C ) )
27 26 ralrexbid 
 |-  ( A. i e. I D e. W -> ( E. i e. I E. y ( z = C /\ y = D ) <-> E. i e. I z = C ) )
28 27 adantl 
 |-  ( ( A. v e. V B e. X /\ A. i e. I D e. W ) -> ( E. i e. I E. y ( z = C /\ y = D ) <-> E. i e. I z = C ) )
29 18 28 orbi12d 
 |-  ( ( A. v e. V B e. X /\ A. i e. I D e. W ) -> ( ( E. v e. V E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) <-> ( E. v e. V z = A \/ E. i e. I z = C ) ) )
30 29 ralrexbid 
 |-  ( A. u e. U ( A. v e. V B e. X /\ A. i e. I D e. W ) -> ( E. u e. U ( E. v e. V E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) <-> E. u e. U ( E. v e. V z = A \/ E. i e. I z = C ) ) )
31 8 30 bitr3id 
 |-  ( A. u e. U ( A. v e. V B e. X /\ A. i e. I D e. W ) -> ( E. y E. u e. U ( E. v e. V ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) <-> E. u e. U ( E. v e. V z = A \/ E. i e. 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 -> ( E. v e. V ( x = A /\ y = B ) <-> E. v e. 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 -> ( E. i e. I ( x = C /\ y = D ) <-> E. i e. I ( z = C /\ y = D ) ) )
38 34 37 orbi12d 
 |-  ( x = z -> ( ( E. v e. V ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) <-> ( E. v e. V ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) ) )
39 38 rexbidv 
 |-  ( x = z -> ( E. u e. U ( E. v e. V ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) <-> E. u e. U ( E. v e. V ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) ) )
40 39 dmopabelb 
 |-  ( z e. _V -> ( z e. dom { <. x , y >. | E. u e. U ( E. v e. V ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) } <-> E. y E. u e. U ( E. v e. V ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) ) )
41 40 elv 
 |-  ( z e. dom { <. x , y >. | E. u e. U ( E. v e. V ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) } <-> E. y E. u e. U ( E. v e. V ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) )
42 vex 
 |-  z e. _V
43 32 rexbidv 
 |-  ( x = z -> ( E. v e. V x = A <-> E. v e. V z = A ) )
44 35 rexbidv 
 |-  ( x = z -> ( E. i e. I x = C <-> E. i e. I z = C ) )
45 43 44 orbi12d 
 |-  ( x = z -> ( ( E. v e. V x = A \/ E. i e. I x = C ) <-> ( E. v e. V z = A \/ E. i e. I z = C ) ) )
46 45 rexbidv 
 |-  ( x = z -> ( E. u e. U ( E. v e. V x = A \/ E. i e. I x = C ) <-> E. u e. U ( E. v e. V z = A \/ E. i e. I z = C ) ) )
47 42 46 elab 
 |-  ( z e. { x | E. u e. U ( E. v e. V x = A \/ E. i e. I x = C ) } <-> E. u e. U ( E. v e. V z = A \/ E. i e. I z = C ) )
48 31 41 47 3bitr4g 
 |-  ( A. u e. U ( A. v e. V B e. X /\ A. i e. I D e. W ) -> ( z e. dom { <. x , y >. | E. u e. U ( E. v e. V ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) } <-> z e. { x | E. u e. U ( E. v e. V x = A \/ E. i e. I x = C ) } ) )
49 48 eqrdv 
 |-  ( A. u e. U ( A. v e. V B e. X /\ A. i e. I D e. W ) -> dom { <. x , y >. | E. u e. U ( E. v e. V ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) } = { x | E. u e. U ( E. v e. V x = A \/ E. i e. I x = C ) } )