copsex2b

Description: Biconditional form of copsex2d . TODO: prove a relative version, that is, with E. x e. V E. y e. W ... ( A e. V /\ B e. W ) . (Contributed by BJ, 27-Dec-2023)

	Ref	Expression
Hypotheses	copsex2b.xph	\|- ( ph -> A. x ph )
	copsex2b.yph	\|- ( ph -> A. y ph )
	copsex2b.xch	\|- ( ph -> F/ x ch )
	copsex2b.ych	\|- ( ph -> F/ y ch )
	copsex2b.is	\|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
Assertion	copsex2b	\|- ( ph -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ( ( A e. _V /\ B e. _V ) /\ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		copsex2b.xph	\|- ( ph -> A. x ph )
2		copsex2b.yph	\|- ( ph -> A. y ph )
3		copsex2b.xch	\|- ( ph -> F/ x ch )
4		copsex2b.ych	\|- ( ph -> F/ y ch )
5		copsex2b.is	\|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
6		eqcom	\|- ( <. A , B >. = <. x , y >. <-> <. x , y >. = <. A , B >. )
7		vex	\|- x e. _V
8		vex	\|- y e. _V
9	7 8	opth	\|- ( <. x , y >. = <. A , B >. <-> ( x = A /\ y = B ) )
10	6 9	bitri	\|- ( <. A , B >. = <. x , y >. <-> ( x = A /\ y = B ) )
11		eqvisset	\|- ( x = A -> A e. _V )
12		eqvisset	\|- ( y = B -> B e. _V )
13	11 12	anim12i	\|- ( ( x = A /\ y = B ) -> ( A e. _V /\ B e. _V ) )
14	10 13	sylbi	\|- ( <. A , B >. = <. x , y >. -> ( A e. _V /\ B e. _V ) )
15	14	adantr	\|- ( ( <. A , B >. = <. x , y >. /\ ps ) -> ( A e. _V /\ B e. _V ) )
16	15	exlimivv	\|- ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) -> ( A e. _V /\ B e. _V ) )
17	16	anim2i	\|- ( ( ph /\ E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) ) -> ( ph /\ ( A e. _V /\ B e. _V ) ) )
18		simpl	\|- ( ( ( A e. _V /\ B e. _V ) /\ ch ) -> ( A e. _V /\ B e. _V ) )
19	18	anim2i	\|- ( ( ph /\ ( ( A e. _V /\ B e. _V ) /\ ch ) ) -> ( ph /\ ( A e. _V /\ B e. _V ) ) )
20		ax-5	\|- ( ( A e. _V /\ B e. _V ) -> A. x ( A e. _V /\ B e. _V ) )
21	1 20	hban	\|- ( ( ph /\ ( A e. _V /\ B e. _V ) ) -> A. x ( ph /\ ( A e. _V /\ B e. _V ) ) )
22		ax-5	\|- ( ( A e. _V /\ B e. _V ) -> A. y ( A e. _V /\ B e. _V ) )
23	2 22	hban	\|- ( ( ph /\ ( A e. _V /\ B e. _V ) ) -> A. y ( ph /\ ( A e. _V /\ B e. _V ) ) )
24	3	adantr	\|- ( ( ph /\ ( A e. _V /\ B e. _V ) ) -> F/ x ch )
25	4	adantr	\|- ( ( ph /\ ( A e. _V /\ B e. _V ) ) -> F/ y ch )
26		simprl	\|- ( ( ph /\ ( A e. _V /\ B e. _V ) ) -> A e. _V )
27		simprr	\|- ( ( ph /\ ( A e. _V /\ B e. _V ) ) -> B e. _V )
28	5	adantlr	\|- ( ( ( ph /\ ( A e. _V /\ B e. _V ) ) /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
29	21 23 24 25 26 27 28	copsex2d	\|- ( ( ph /\ ( A e. _V /\ B e. _V ) ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ch ) )
30		ibar	\|- ( ( A e. _V /\ B e. _V ) -> ( ch <-> ( ( A e. _V /\ B e. _V ) /\ ch ) ) )
31	30	adantl	\|- ( ( ph /\ ( A e. _V /\ B e. _V ) ) -> ( ch <-> ( ( A e. _V /\ B e. _V ) /\ ch ) ) )
32	29 31	bitrd	\|- ( ( ph /\ ( A e. _V /\ B e. _V ) ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ( ( A e. _V /\ B e. _V ) /\ ch ) ) )
33	17 19 32	pm5.21nd	\|- ( ph -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ps ) <-> ( ( A e. _V /\ B e. _V ) /\ ch ) ) )

Metamath Proof Explorer

Theorem copsex2b

Proof