This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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