Metamath Proof Explorer

Theorem isfrgr

Description: The property of being a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017) (Revised by AV, 29-Mar-2021) (Revised by AV, 3-Jan-2024)

Ref Expression
Hypotheses isfrgr.v 
|- V = ( Vtx ` G )
isfrgr.e 
|- E = ( Edg ` G )
Assertion isfrgr 
|- ( G e. FriendGraph <-> ( G e. USGraph /\ A. k e. V A. l e. ( V \ { k } ) E! x e. V { { x , k } , { x , l } } C_ E ) )

Proof

Step Hyp Ref Expression
1 isfrgr.v 
 |-  V = ( Vtx ` G )
2 isfrgr.e 
 |-  E = ( Edg ` G )
3 fvex 
 |-  ( Vtx ` g ) e. _V
4 fvex 
 |-  ( Edg ` g ) e. _V
5 fveq2 
 |-  ( g = G -> ( Vtx ` g ) = ( Vtx ` G ) )
6 5 eqeq2d 
 |-  ( g = G -> ( v = ( Vtx ` g ) <-> v = ( Vtx ` G ) ) )
7 1 eqcomi 
 |-  ( Vtx ` G ) = V
8 7 eqeq2i 
 |-  ( v = ( Vtx ` G ) <-> v = V )
9 6 8 bitrdi 
 |-  ( g = G -> ( v = ( Vtx ` g ) <-> v = V ) )
10 fveq2 
 |-  ( g = G -> ( Edg ` g ) = ( Edg ` G ) )
11 10 eqeq2d 
 |-  ( g = G -> ( e = ( Edg ` g ) <-> e = ( Edg ` G ) ) )
12 2 eqcomi 
 |-  ( Edg ` G ) = E
13 12 eqeq2i 
 |-  ( e = ( Edg ` G ) <-> e = E )
14 11 13 bitrdi 
 |-  ( g = G -> ( e = ( Edg ` g ) <-> e = E ) )
15 9 14 anbi12d 
 |-  ( g = G -> ( ( v = ( Vtx ` g ) /\ e = ( Edg ` g ) ) <-> ( v = V /\ e = E ) ) )
16 simpl 
 |-  ( ( v = V /\ e = E ) -> v = V )
17 difeq1 
 |-  ( v = V -> ( v \ { k } ) = ( V \ { k } ) )
18 17 adantr 
 |-  ( ( v = V /\ e = E ) -> ( v \ { k } ) = ( V \ { k } ) )
19 reueq1 
 |-  ( v = V -> ( E! x e. v { { x , k } , { x , l } } C_ e <-> E! x e. V { { x , k } , { x , l } } C_ e ) )
20 19 adantr 
 |-  ( ( v = V /\ e = E ) -> ( E! x e. v { { x , k } , { x , l } } C_ e <-> E! x e. V { { x , k } , { x , l } } C_ e ) )
21 sseq2 
 |-  ( e = E -> ( { { x , k } , { x , l } } C_ e <-> { { x , k } , { x , l } } C_ E ) )
22 21 adantl 
 |-  ( ( v = V /\ e = E ) -> ( { { x , k } , { x , l } } C_ e <-> { { x , k } , { x , l } } C_ E ) )
23 22 reubidv 
 |-  ( ( v = V /\ e = E ) -> ( E! x e. V { { x , k } , { x , l } } C_ e <-> E! x e. V { { x , k } , { x , l } } C_ E ) )
24 20 23 bitrd 
 |-  ( ( v = V /\ e = E ) -> ( E! x e. v { { x , k } , { x , l } } C_ e <-> E! x e. V { { x , k } , { x , l } } C_ E ) )
25 18 24 raleqbidv 
 |-  ( ( v = V /\ e = E ) -> ( A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e <-> A. l e. ( V \ { k } ) E! x e. V { { x , k } , { x , l } } C_ E ) )
26 16 25 raleqbidv 
 |-  ( ( v = V /\ e = E ) -> ( A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e <-> A. k e. V A. l e. ( V \ { k } ) E! x e. V { { x , k } , { x , l } } C_ E ) )
27 15 26 syl6bi 
 |-  ( g = G -> ( ( v = ( Vtx ` g ) /\ e = ( Edg ` g ) ) -> ( A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e <-> A. k e. V A. l e. ( V \ { k } ) E! x e. V { { x , k } , { x , l } } C_ E ) ) )
28 3 4 27 sbc2iedv 
 |-  ( g = G -> ( [. ( Vtx ` g ) / v ]. [. ( Edg ` g ) / e ]. A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e <-> A. k e. V A. l e. ( V \ { k } ) E! x e. V { { x , k } , { x , l } } C_ E ) )
29 df-frgr 
 |-  FriendGraph = { g e. USGraph | [. ( Vtx ` g ) / v ]. [. ( Edg ` g ) / e ]. A. k e. v A. l e. ( v \ { k } ) E! x e. v { { x , k } , { x , l } } C_ e }
30 28 29 elrab2 
 |-  ( G e. FriendGraph <-> ( G e. USGraph /\ A. k e. V A. l e. ( V \ { k } ) E! x e. V { { x , k } , { x , l } } C_ E ) )