Metamath Proof Explorer

Theorem fvconstr2

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 } ) )
fvconstr2.2 
|- ( ph -> X e. ( A F B ) )
Assertion fvconstr2 
|- ( ph -> A R B )

Proof

Step Hyp Ref Expression
1 fvconstr.1 
 |-  ( ph -> F = ( R X. { Y } ) )
2 fvconstr2.2 
 |-  ( ph -> X e. ( A F B ) )
3 2 ne0d 
 |-  ( ph -> ( A F B ) =/= (/) )
4 1 oveqd 
 |-  ( ph -> ( A F B ) = ( A ( R X. { Y } ) B ) )
5 df-ov 
 |-  ( A ( R X. { Y } ) B ) = ( ( R X. { Y } ) ` <. A , B >. )
6 4 5 eqtrdi 
 |-  ( ph -> ( A F B ) = ( ( R X. { Y } ) ` <. A , B >. ) )
7 6 neeq1d 
 |-  ( ph -> ( ( A F B ) =/= (/) <-> ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) ) )
8 dmxpss 
 |-  dom ( R X. { Y } ) C_ R
9 ndmfv 
 |-  ( -. <. A , B >. e. dom ( R X. { Y } ) -> ( ( R X. { Y } ) ` <. A , B >. ) = (/) )
10 9 necon1ai 
 |-  ( ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) -> <. A , B >. e. dom ( R X. { Y } ) )
11 8 10 sselid 
 |-  ( ( ( R X. { Y } ) ` <. A , B >. ) =/= (/) -> <. A , B >. e. R )
12 7 11 syl6bi 
 |-  ( ph -> ( ( A F B ) =/= (/) -> <. A , B >. e. R ) )
13 3 12 mpd 
 |-  ( ph -> <. A , B >. e. R )
14 df-br 
 |-  ( A R B <-> <. A , B >. e. R )
15 13 14 sylibr 
 |-  ( ph -> A R B )