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 u U v U B X i I D W S U dom x y | u U S v U x = A y = B i I x = C y = D u S v U S x = A y = B = x | u U S v U x = A i I x = C u S v U S x = A

Proof

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