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 ) } )