Metamath Proof Explorer

Theorem frsn

Description: Founded relation on a singleton. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by Mario Carneiro, 23-Apr-2015)

Ref Expression
Assertion frsn 
|- ( Rel R -> ( R Fr { A } <-> -. A R A ) )

Proof

Step Hyp Ref Expression
1 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
2 fr0 
 |-  R Fr (/)
3 freq2 
 |-  ( { A } = (/) -> ( R Fr { A } <-> R Fr (/) ) )
4 2 3 mpbiri 
 |-  ( { A } = (/) -> R Fr { A } )
5 1 4 sylbi 
 |-  ( -. A e. _V -> R Fr { A } )
6 5 adantl 
 |-  ( ( Rel R /\ -. A e. _V ) -> R Fr { A } )
7 brrelex1 
 |-  ( ( Rel R /\ A R A ) -> A e. _V )
8 7 stoic1a 
 |-  ( ( Rel R /\ -. A e. _V ) -> -. A R A )
9 6 8 2thd 
 |-  ( ( Rel R /\ -. A e. _V ) -> ( R Fr { A } <-> -. A R A ) )
10 9 ex 
 |-  ( Rel R -> ( -. A e. _V -> ( R Fr { A } <-> -. A R A ) ) )
11 df-fr 
 |-  ( R Fr { A } <-> A. x ( ( x C_ { A } /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) )
12 sssn 
 |-  ( x C_ { A } <-> ( x = (/) \/ x = { A } ) )
13 neor 
 |-  ( ( x = (/) \/ x = { A } ) <-> ( x =/= (/) -> x = { A } ) )
14 12 13 sylbb 
 |-  ( x C_ { A } -> ( x =/= (/) -> x = { A } ) )
15 14 imp 
 |-  ( ( x C_ { A } /\ x =/= (/) ) -> x = { A } )
16 15 adantl 
 |-  ( ( A e. _V /\ ( x C_ { A } /\ x =/= (/) ) ) -> x = { A } )
17 eqimss 
 |-  ( x = { A } -> x C_ { A } )
18 17 adantl 
 |-  ( ( A e. _V /\ x = { A } ) -> x C_ { A } )
19 snnzg 
 |-  ( A e. _V -> { A } =/= (/) )
20 neeq1 
 |-  ( x = { A } -> ( x =/= (/) <-> { A } =/= (/) ) )
21 19 20 syl5ibrcom 
 |-  ( A e. _V -> ( x = { A } -> x =/= (/) ) )
22 21 imp 
 |-  ( ( A e. _V /\ x = { A } ) -> x =/= (/) )
23 18 22 jca 
 |-  ( ( A e. _V /\ x = { A } ) -> ( x C_ { A } /\ x =/= (/) ) )
24 16 23 impbida 
 |-  ( A e. _V -> ( ( x C_ { A } /\ x =/= (/) ) <-> x = { A } ) )
25 24 imbi1d 
 |-  ( A e. _V -> ( ( ( x C_ { A } /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) <-> ( x = { A } -> E. y e. x A. z e. x -. z R y ) ) )
26 25 albidv 
 |-  ( A e. _V -> ( A. x ( ( x C_ { A } /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) <-> A. x ( x = { A } -> E. y e. x A. z e. x -. z R y ) ) )
27 snex 
 |-  { A } e. _V
28 raleq 
 |-  ( x = { A } -> ( A. z e. x -. z R y <-> A. z e. { A } -. z R y ) )
29 28 rexeqbi1dv 
 |-  ( x = { A } -> ( E. y e. x A. z e. x -. z R y <-> E. y e. { A } A. z e. { A } -. z R y ) )
30 27 29 ceqsalv 
 |-  ( A. x ( x = { A } -> E. y e. x A. z e. x -. z R y ) <-> E. y e. { A } A. z e. { A } -. z R y )
31 26 30 bitrdi 
 |-  ( A e. _V -> ( A. x ( ( x C_ { A } /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) <-> E. y e. { A } A. z e. { A } -. z R y ) )
32 11 31 bitrid 
 |-  ( A e. _V -> ( R Fr { A } <-> E. y e. { A } A. z e. { A } -. z R y ) )
33 breq2 
 |-  ( y = A -> ( z R y <-> z R A ) )
34 33 notbid 
 |-  ( y = A -> ( -. z R y <-> -. z R A ) )
35 34 ralbidv 
 |-  ( y = A -> ( A. z e. { A } -. z R y <-> A. z e. { A } -. z R A ) )
36 35 rexsng 
 |-  ( A e. _V -> ( E. y e. { A } A. z e. { A } -. z R y <-> A. z e. { A } -. z R A ) )
37 breq1 
 |-  ( z = A -> ( z R A <-> A R A ) )
38 37 notbid 
 |-  ( z = A -> ( -. z R A <-> -. A R A ) )
39 38 ralsng 
 |-  ( A e. _V -> ( A. z e. { A } -. z R A <-> -. A R A ) )
40 32 36 39 3bitrd 
 |-  ( A e. _V -> ( R Fr { A } <-> -. A R A ) )
41 10 40 pm2.61d2 
 |-  ( Rel R -> ( R Fr { A } <-> -. A R A ) )