Definition df-frgr

Description: Define the class of all friendship graphs: a simple graph is called a friendship graph if every pair of its vertices has exactly one common neighbor. This condition is called thefriendship condition , see definition in MertziosUnger p. 152. (Contributed by Alexander van der Vekens and Mario Carneiro, 2-Oct-2017) (Revised by AV, 29-Mar-2021) (Revised by AV, 3-Jan-2024)

	Ref	Expression
Assertion	df-frgr	⊢ FriendGraph = { 𝑔 ∈ USGraph ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( Edg ‘ 𝑔 ) / 𝑒 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑙 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfrgr	⊢ FriendGraph
1		vg	⊢ 𝑔
2		cusgr	⊢ USGraph
3		cvtx	⊢ Vtx
4	1	cv	⊢ 𝑔
5	4 3	cfv	⊢ ( Vtx ‘ 𝑔 )
6		vv	⊢ 𝑣
7		cedg	⊢ Edg
8	4 7	cfv	⊢ ( Edg ‘ 𝑔 )
9		ve	⊢ 𝑒
10		vk	⊢ 𝑘
11	6	cv	⊢ 𝑣
12		vl	⊢ 𝑙
13	10	cv	⊢ 𝑘
14	13	csn	⊢ { 𝑘 }
15	11 14	cdif	⊢ ( 𝑣 ∖ { 𝑘 } )
16		vx	⊢ 𝑥
17	16	cv	⊢ 𝑥
18	17 13	cpr	⊢ { 𝑥 , 𝑘 }
19	12	cv	⊢ 𝑙
20	17 19	cpr	⊢ { 𝑥 , 𝑙 }
21	18 20	cpr	⊢ { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } }
22	9	cv	⊢ 𝑒
23	21 22	wss	⊢ { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒
24	23 16 11	wreu	⊢ ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒
25	24 12 15	wral	⊢ ∀ 𝑙 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒
26	25 10 11	wral	⊢ ∀ 𝑘 ∈ 𝑣 ∀ 𝑙 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒
27	26 9 8	wsbc	⊢ [ ( Edg ‘ 𝑔 ) / 𝑒 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑙 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒
28	27 6 5	wsbc	⊢ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( Edg ‘ 𝑔 ) / 𝑒 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑙 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒
29	28 1 2	crab	⊢ { 𝑔 ∈ USGraph ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( Edg ‘ 𝑔 ) / 𝑒 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑙 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 }
30	0 29	wceq	⊢ FriendGraph = { 𝑔 ∈ USGraph ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( Edg ‘ 𝑔 ) / 𝑒 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑙 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 }