Theorem fvconstr

Description: Two ways of expressing A R B . (Contributed by Zhi Wang, 18-Sep-2024)

	Ref	Expression
Hypotheses	fvconstr.1	|- ( ph -> F = ( R X. { Y } ) )
	fvconstr.2	|- ( ph -> Y e. V )
	fvconstr.3	|- ( ph -> Y =/= (/) )
Assertion	fvconstr	|- ( ph -> ( A R B <-> ( A F B ) = Y ) )

Proof

Step	Hyp	Ref	Expression
1		fvconstr.1	|- ( ph -> F = ( R X. { Y } ) )
2		fvconstr.2	|- ( ph -> Y e. V )
3		fvconstr.3	|- ( ph -> Y =/= (/) )
4		df-br	|- ( A R B <-> <. A , B >. e. R )
5	1	oveqd	|- ( ph -> ( A F B ) = ( A ( R X. { Y } ) B ) )
6		df-ov	|- ( A ( R X. { Y } ) B ) = ( ( R X. { Y } ) ` <. A , B >. )
7	5 6	eqtrdi	|- ( ph -> ( A F B ) = ( ( R X. { Y } ) ` <. A , B >. ) )
8	7	adantr	|- ( ( ph /\ <. A , B >. e. R ) -> ( A F B ) = ( ( R X. { Y } ) ` <. A , B >. ) )
9		fvconst2g	|- ( ( Y e. V /\ <. A , B >. e. R ) -> ( ( R X. { Y } ) ` <. A , B >. ) = Y )
10	2 9	sylan	|- ( ( ph /\ <. A , B >. e. R ) -> ( ( R X. { Y } ) ` <. A , B >. ) = Y )
11	8 10	eqtrd	|- ( ( ph /\ <. A , B >. e. R ) -> ( A F B ) = Y )
12		simpr	|- ( ( ph /\ ( A F B ) = Y ) -> ( A F B ) = Y )
13	3	adantr	|- ( ( ph /\ ( A F B ) = Y ) -> Y =/= (/) )
14	12 13	eqnetrd	|- ( ( ph /\ ( A F B ) = Y ) -> ( A F B ) =/= (/) )
15	7	neeq1d	|- ( ph -> ( ( A F B ) =/= (/) <-> ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) ) )
16	15	adantr	|- ( ( ph /\ ( A F B ) = Y ) -> ( ( A F B ) =/= (/) <-> ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) ) )
17	14 16	mpbid	|- ( ( ph /\ ( A F B ) = Y ) -> ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) )
18		dmxpss	|- dom ( R X. { Y } ) C_ R
19		ndmfv	|- ( -. <. A , B >. e. dom ( R X. { Y } ) -> ( ( R X. { Y } ) ` <. A , B >. ) = (/) )
20	19	necon1ai	|- ( ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) -> <. A , B >. e. dom ( R X. { Y } ) )
21	18 20	sselid	|- ( ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) -> <. A , B >. e. R )
22	17 21	syl	|- ( ( ph /\ ( A F B ) = Y ) -> <. A , B >. e. R )
23	11 22	impbida	|- ( ph -> ( <. A , B >. e. R <-> ( A F B ) = Y ) )
24	4 23	bitrid	|- ( ph -> ( A R B <-> ( A F B ) = Y ) )