Metamath Proof Explorer

Theorem dmopab3rexdif

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

Ref Expression
Assertion dmopab3rexdif 
|- ( ( A. u e. U ( A. v e. U B e. X /\ A. i e. I D e. W ) /\ S C_ U ) -> dom { <. x , y >. | ( E. u e. ( U \ S ) ( E. v e. U ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) ( x = A /\ y = B ) ) } = { x | ( E. u e. ( U \ S ) ( E. v e. U x = A \/ E. i e. I x = C ) \/ E. u e. S E. v e. ( U \ S ) x = A ) } )

Proof

Step Hyp Ref Expression
1 rexcom4 
 |-  ( E. v e. U E. y ( z = A /\ y = B ) <-> E. y E. v e. U ( 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. U E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) <-> ( E. y E. v e. U ( z = A /\ y = B ) \/ E. y E. i e. I ( z = C /\ y = D ) ) )
4 19.43 
 |-  ( E. y ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) <-> ( E. y E. v e. U ( z = A /\ y = B ) \/ E. y E. i e. I ( z = C /\ y = D ) ) )
5 3 4 bitr4i 
 |-  ( ( E. v e. U E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) <-> E. y ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) )
6 5 rexbii 
 |-  ( E. u e. ( U \ S ) ( E. v e. U E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) <-> E. u e. ( U \ S ) E. y ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) )
7 rexcom4 
 |-  ( E. u e. ( U \ S ) E. y ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) <-> E. y E. u e. ( U \ S ) ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) )
8 6 7 bitri 
 |-  ( E. u e. ( U \ S ) ( E. v e. U E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) <-> E. y E. u e. ( U \ S ) ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) )
9 rexcom4 
 |-  ( E. v e. ( U \ S ) E. y ( z = A /\ y = B ) <-> E. y E. v e. ( U \ S ) ( z = A /\ y = B ) )
10 9 rexbii 
 |-  ( E. u e. S E. v e. ( U \ S ) E. y ( z = A /\ y = B ) <-> E. u e. S E. y E. v e. ( U \ S ) ( z = A /\ y = B ) )
11 rexcom4 
 |-  ( E. u e. S E. y E. v e. ( U \ S ) ( z = A /\ y = B ) <-> E. y E. u e. S E. v e. ( U \ S ) ( z = A /\ y = B ) )
12 10 11 bitri 
 |-  ( E. u e. S E. v e. ( U \ S ) E. y ( z = A /\ y = B ) <-> E. y E. u e. S E. v e. ( U \ S ) ( z = A /\ y = B ) )
13 8 12 orbi12i 
 |-  ( ( E. u e. ( U \ S ) ( E. v e. U E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) E. y ( z = A /\ y = B ) ) <-> ( E. y E. u e. ( U \ S ) ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) \/ E. y E. u e. S E. v e. ( U \ S ) ( z = A /\ y = B ) ) )
14 19.43 
 |-  ( E. y ( E. u e. ( U \ S ) ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) ( z = A /\ y = B ) ) <-> ( E. y E. u e. ( U \ S ) ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) \/ E. y E. u e. S E. v e. ( U \ S ) ( z = A /\ y = B ) ) )
15 13 14 bitr4i 
 |-  ( ( E. u e. ( U \ S ) ( E. v e. U E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) E. y ( z = A /\ y = B ) ) <-> E. y ( E. u e. ( U \ S ) ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) ( z = A /\ y = B ) ) )
16 difssd 
 |-  ( S C_ U -> ( U \ S ) C_ U )
17 ssralv 
 |-  ( ( U \ S ) C_ U -> ( A. u e. U ( A. v e. U B e. X /\ A. i e. I D e. W ) -> A. u e. ( U \ S ) ( A. v e. U B e. X /\ A. i e. I D e. W ) ) )
18 16 17 syl 
 |-  ( S C_ U -> ( A. u e. U ( A. v e. U B e. X /\ A. i e. I D e. W ) -> A. u e. ( U \ S ) ( A. v e. U B e. X /\ A. i e. I D e. W ) ) )
19 18 impcom 
 |-  ( ( A. u e. U ( A. v e. U B e. X /\ A. i e. I D e. W ) /\ S C_ U ) -> A. u e. ( U \ S ) ( A. v e. U B e. X /\ A. i e. I D e. W ) )
20 simpl 
 |-  ( ( z = A /\ y = B ) -> z = A )
21 20 exlimiv 
 |-  ( E. y ( z = A /\ y = B ) -> z = A )
22 elisset 
 |-  ( B e. X -> E. y y = B )
23 ibar 
 |-  ( z = A -> ( y = B <-> ( z = A /\ y = B ) ) )
24 23 bicomd 
 |-  ( z = A -> ( ( z = A /\ y = B ) <-> y = B ) )
25 24 exbidv 
 |-  ( z = A -> ( E. y ( z = A /\ y = B ) <-> E. y y = B ) )
26 22 25 syl5ibrcom 
 |-  ( B e. X -> ( z = A -> E. y ( z = A /\ y = B ) ) )
27 21 26 impbid2 
 |-  ( B e. X -> ( E. y ( z = A /\ y = B ) <-> z = A ) )
28 27 ralrexbid 
 |-  ( A. v e. U B e. X -> ( E. v e. U E. y ( z = A /\ y = B ) <-> E. v e. U z = A ) )
29 28 adantr 
 |-  ( ( A. v e. U B e. X /\ A. i e. I D e. W ) -> ( E. v e. U E. y ( z = A /\ y = B ) <-> E. v e. U z = A ) )
30 simpl 
 |-  ( ( z = C /\ y = D ) -> z = C )
31 30 exlimiv 
 |-  ( E. y ( z = C /\ y = D ) -> z = C )
32 elisset 
 |-  ( D e. W -> E. y y = D )
33 ibar 
 |-  ( z = C -> ( y = D <-> ( z = C /\ y = D ) ) )
34 33 bicomd 
 |-  ( z = C -> ( ( z = C /\ y = D ) <-> y = D ) )
35 34 exbidv 
 |-  ( z = C -> ( E. y ( z = C /\ y = D ) <-> E. y y = D ) )
36 32 35 syl5ibrcom 
 |-  ( D e. W -> ( z = C -> E. y ( z = C /\ y = D ) ) )
37 31 36 impbid2 
 |-  ( D e. W -> ( E. y ( z = C /\ y = D ) <-> z = C ) )
38 37 ralrexbid 
 |-  ( A. i e. I D e. W -> ( E. i e. I E. y ( z = C /\ y = D ) <-> E. i e. I z = C ) )
39 38 adantl 
 |-  ( ( A. v e. U 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 ) )
40 29 39 orbi12d 
 |-  ( ( A. v e. U B e. X /\ A. i e. I D e. W ) -> ( ( E. v e. U E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) <-> ( E. v e. U z = A \/ E. i e. I z = C ) ) )
41 40 ralrexbid 
 |-  ( A. u e. ( U \ S ) ( A. v e. U B e. X /\ A. i e. I D e. W ) -> ( E. u e. ( U \ S ) ( E. v e. U E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) <-> E. u e. ( U \ S ) ( E. v e. U z = A \/ E. i e. I z = C ) ) )
42 19 41 syl 
 |-  ( ( A. u e. U ( A. v e. U B e. X /\ A. i e. I D e. W ) /\ S C_ U ) -> ( E. u e. ( U \ S ) ( E. v e. U E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) <-> E. u e. ( U \ S ) ( E. v e. U z = A \/ E. i e. I z = C ) ) )
43 ssralv 
 |-  ( S C_ U -> ( A. u e. U ( A. v e. U B e. X /\ A. i e. I D e. W ) -> A. u e. S ( A. v e. U B e. X /\ A. i e. I D e. W ) ) )
44 ssralv 
 |-  ( ( U \ S ) C_ U -> ( A. v e. U B e. X -> A. v e. ( U \ S ) B e. X ) )
45 16 44 syl 
 |-  ( S C_ U -> ( A. v e. U B e. X -> A. v e. ( U \ S ) B e. X ) )
46 45 adantrd 
 |-  ( S C_ U -> ( ( A. v e. U B e. X /\ A. i e. I D e. W ) -> A. v e. ( U \ S ) B e. X ) )
47 46 ralimdv 
 |-  ( S C_ U -> ( A. u e. S ( A. v e. U B e. X /\ A. i e. I D e. W ) -> A. u e. S A. v e. ( U \ S ) B e. X ) )
48 43 47 syld 
 |-  ( S C_ U -> ( A. u e. U ( A. v e. U B e. X /\ A. i e. I D e. W ) -> A. u e. S A. v e. ( U \ S ) B e. X ) )
49 48 impcom 
 |-  ( ( A. u e. U ( A. v e. U B e. X /\ A. i e. I D e. W ) /\ S C_ U ) -> A. u e. S A. v e. ( U \ S ) B e. X )
50 27 ralrexbid 
 |-  ( A. v e. ( U \ S ) B e. X -> ( E. v e. ( U \ S ) E. y ( z = A /\ y = B ) <-> E. v e. ( U \ S ) z = A ) )
51 50 ralrexbid 
 |-  ( A. u e. S A. v e. ( U \ S ) B e. X -> ( E. u e. S E. v e. ( U \ S ) E. y ( z = A /\ y = B ) <-> E. u e. S E. v e. ( U \ S ) z = A ) )
52 49 51 syl 
 |-  ( ( A. u e. U ( A. v e. U B e. X /\ A. i e. I D e. W ) /\ S C_ U ) -> ( E. u e. S E. v e. ( U \ S ) E. y ( z = A /\ y = B ) <-> E. u e. S E. v e. ( U \ S ) z = A ) )
53 42 52 orbi12d 
 |-  ( ( A. u e. U ( A. v e. U B e. X /\ A. i e. I D e. W ) /\ S C_ U ) -> ( ( E. u e. ( U \ S ) ( E. v e. U E. y ( z = A /\ y = B ) \/ E. i e. I E. y ( z = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) E. y ( z = A /\ y = B ) ) <-> ( E. u e. ( U \ S ) ( E. v e. U z = A \/ E. i e. I z = C ) \/ E. u e. S E. v e. ( U \ S ) z = A ) ) )
54 15 53 bitr3id 
 |-  ( ( A. u e. U ( A. v e. U B e. X /\ A. i e. I D e. W ) /\ S C_ U ) -> ( E. y ( E. u e. ( U \ S ) ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) ( z = A /\ y = B ) ) <-> ( E. u e. ( U \ S ) ( E. v e. U z = A \/ E. i e. I z = C ) \/ E. u e. S E. v e. ( U \ S ) z = A ) ) )
55 eqeq1 
 |-  ( x = z -> ( x = A <-> z = A ) )
56 55 anbi1d 
 |-  ( x = z -> ( ( x = A /\ y = B ) <-> ( z = A /\ y = B ) ) )
57 56 rexbidv 
 |-  ( x = z -> ( E. v e. U ( x = A /\ y = B ) <-> E. v e. U ( z = A /\ y = B ) ) )
58 eqeq1 
 |-  ( x = z -> ( x = C <-> z = C ) )
59 58 anbi1d 
 |-  ( x = z -> ( ( x = C /\ y = D ) <-> ( z = C /\ y = D ) ) )
60 59 rexbidv 
 |-  ( x = z -> ( E. i e. I ( x = C /\ y = D ) <-> E. i e. I ( z = C /\ y = D ) ) )
61 57 60 orbi12d 
 |-  ( x = z -> ( ( E. v e. U ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) <-> ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) ) )
62 61 rexbidv 
 |-  ( x = z -> ( E. u e. ( U \ S ) ( E. v e. U ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) <-> E. u e. ( U \ S ) ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) ) )
63 56 2rexbidv 
 |-  ( x = z -> ( E. u e. S E. v e. ( U \ S ) ( x = A /\ y = B ) <-> E. u e. S E. v e. ( U \ S ) ( z = A /\ y = B ) ) )
64 62 63 orbi12d 
 |-  ( x = z -> ( ( E. u e. ( U \ S ) ( E. v e. U ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) ( x = A /\ y = B ) ) <-> ( E. u e. ( U \ S ) ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) ( z = A /\ y = B ) ) ) )
65 64 dmopabelb 
 |-  ( z e. _V -> ( z e. dom { <. x , y >. | ( E. u e. ( U \ S ) ( E. v e. U ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) ( x = A /\ y = B ) ) } <-> E. y ( E. u e. ( U \ S ) ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) ( z = A /\ y = B ) ) ) )
66 65 elv 
 |-  ( z e. dom { <. x , y >. | ( E. u e. ( U \ S ) ( E. v e. U ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) ( x = A /\ y = B ) ) } <-> E. y ( E. u e. ( U \ S ) ( E. v e. U ( z = A /\ y = B ) \/ E. i e. I ( z = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) ( z = A /\ y = B ) ) )
67 vex 
 |-  z e. _V
68 55 rexbidv 
 |-  ( x = z -> ( E. v e. U x = A <-> E. v e. U z = A ) )
69 58 rexbidv 
 |-  ( x = z -> ( E. i e. I x = C <-> E. i e. I z = C ) )
70 68 69 orbi12d 
 |-  ( x = z -> ( ( E. v e. U x = A \/ E. i e. I x = C ) <-> ( E. v e. U z = A \/ E. i e. I z = C ) ) )
71 70 rexbidv 
 |-  ( x = z -> ( E. u e. ( U \ S ) ( E. v e. U x = A \/ E. i e. I x = C ) <-> E. u e. ( U \ S ) ( E. v e. U z = A \/ E. i e. I z = C ) ) )
72 55 2rexbidv 
 |-  ( x = z -> ( E. u e. S E. v e. ( U \ S ) x = A <-> E. u e. S E. v e. ( U \ S ) z = A ) )
73 71 72 orbi12d 
 |-  ( x = z -> ( ( E. u e. ( U \ S ) ( E. v e. U x = A \/ E. i e. I x = C ) \/ E. u e. S E. v e. ( U \ S ) x = A ) <-> ( E. u e. ( U \ S ) ( E. v e. U z = A \/ E. i e. I z = C ) \/ E. u e. S E. v e. ( U \ S ) z = A ) ) )
74 67 73 elab 
 |-  ( z e. { x | ( E. u e. ( U \ S ) ( E. v e. U x = A \/ E. i e. I x = C ) \/ E. u e. S E. v e. ( U \ S ) x = A ) } <-> ( E. u e. ( U \ S ) ( E. v e. U z = A \/ E. i e. I z = C ) \/ E. u e. S E. v e. ( U \ S ) z = A ) )
75 54 66 74 3bitr4g 
 |-  ( ( A. u e. U ( A. v e. U B e. X /\ A. i e. I D e. W ) /\ S C_ U ) -> ( z e. dom { <. x , y >. | ( E. u e. ( U \ S ) ( E. v e. U ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) ( x = A /\ y = B ) ) } <-> z e. { x | ( E. u e. ( U \ S ) ( E. v e. U x = A \/ E. i e. I x = C ) \/ E. u e. S E. v e. ( U \ S ) x = A ) } ) )
76 75 eqrdv 
 |-  ( ( A. u e. U ( A. v e. U B e. X /\ A. i e. I D e. W ) /\ S C_ U ) -> dom { <. x , y >. | ( E. u e. ( U \ S ) ( E. v e. U ( x = A /\ y = B ) \/ E. i e. I ( x = C /\ y = D ) ) \/ E. u e. S E. v e. ( U \ S ) ( x = A /\ y = B ) ) } = { x | ( E. u e. ( U \ S ) ( E. v e. U x = A \/ E. i e. I x = C ) \/ E. u e. S E. v e. ( U \ S ) x = A ) } )