Metamath Proof Explorer

Theorem fvconstrn0

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

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

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 3 adantr 
 |-  ( ( ph /\ <. A , B >. e. R ) -> Y =/= (/) )
13 11 12 eqnetrd 
 |-  ( ( ph /\ <. A , B >. e. R ) -> ( A F B ) =/= (/) )
14 7 neeq1d 
 |-  ( ph -> ( ( A F B ) =/= (/) <-> ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) ) )
15 14 biimpa 
 |-  ( ( ph /\ ( A F B ) =/= (/) ) -> ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) )
16 dmxpss 
 |-  dom ( R X. { Y } ) C_ R
17 ndmfv 
 |-  ( -. <. A , B >. e. dom ( R X. { Y } ) -> ( ( R X. { Y } ) ` <. A , B >. ) = (/) )
18 17 necon1ai 
 |-  ( ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) -> <. A , B >. e. dom ( R X. { Y } ) )
19 16 18 sseldi 
 |-  ( ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) -> <. A , B >. e. R )
20 15 19 syl 
 |-  ( ( ph /\ ( A F B ) =/= (/) ) -> <. A , B >. e. R )
21 13 20 impbida 
 |-  ( ph -> ( <. A , B >. e. R <-> ( A F B ) =/= (/) ) )
22 4 21 syl5bb 
 |-  ( ph -> ( A R B <-> ( A F B ) =/= (/) ) )