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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isfrgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion isfrgr ( 𝐺 ∈ FriendGraph ↔ ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 isfrgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isfrgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 fvex ⊢ ( Vtx ‘ 𝑔 ) ∈ V
4 fvex ⊢ ( Edg ‘ 𝑔 ) ∈ V
5 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
6 5 eqeq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑣 = ( Vtx ‘ 𝑔 ) ↔ 𝑣 = ( Vtx ‘ 𝐺 ) ) )
7 1 eqcomi ⊢ ( Vtx ‘ 𝐺 ) = 𝑉
8 7 eqeq2i ⊢ ( 𝑣 = ( Vtx ‘ 𝐺 ) ↔ 𝑣 = 𝑉 )
9 6 8 bitrdi ⊢ ( 𝑔 = 𝐺 → ( 𝑣 = ( Vtx ‘ 𝑔 ) ↔ 𝑣 = 𝑉 ) )
10 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Edg ‘ 𝑔 ) = ( Edg ‘ 𝐺 ) )
11 10 eqeq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑒 = ( Edg ‘ 𝑔 ) ↔ 𝑒 = ( Edg ‘ 𝐺 ) ) )
12 2 eqcomi ⊢ ( Edg ‘ 𝐺 ) = 𝐸
13 12 eqeq2i ⊢ ( 𝑒 = ( Edg ‘ 𝐺 ) ↔ 𝑒 = 𝐸 )
14 11 13 bitrdi ⊢ ( 𝑔 = 𝐺 → ( 𝑒 = ( Edg ‘ 𝑔 ) ↔ 𝑒 = 𝐸 ) )
15 9 14 anbi12d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑣 = ( Vtx ‘ 𝑔 ) ∧ 𝑒 = ( Edg ‘ 𝑔 ) ) ↔ ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) ) )
16 simpl ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → 𝑣 = 𝑉 )
17 difeq1 ⊢ ( 𝑣 = 𝑉 → ( 𝑣 ∖ { 𝑘 } ) = ( 𝑉 ∖ { 𝑘 } ) )
18 17 adantr ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝑣 ∖ { 𝑘 } ) = ( 𝑉 ∖ { 𝑘 } ) )
19 reueq1 ⊢ ( 𝑣 = 𝑉 → ( ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 ↔ ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 ) )
20 19 adantr ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 ↔ ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 ) )
21 sseq2 ⊢ ( 𝑒 = 𝐸 → ( { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 ↔ { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
22 21 adantl ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 ↔ { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
23 22 reubidv ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 ↔ ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
24 20 23 bitrd ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 ↔ ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
25 18 24 raleqbidv ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( ∀ 𝑙 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 ↔ ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
26 16 25 raleqbidv ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( ∀ 𝑘 ∈ 𝑣 ∀ 𝑙 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 ↔ ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
27 15 26 syl6bi ⊢ ( 𝑔 = 𝐺 → ( ( 𝑣 = ( Vtx ‘ 𝑔 ) ∧ 𝑒 = ( Edg ‘ 𝑔 ) ) → ( ∀ 𝑘 ∈ 𝑣 ∀ 𝑙 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 ↔ ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) ) )
28 3 4 27 sbc2iedv ⊢ ( 𝑔 = 𝐺 → ( [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( Edg ‘ 𝑔 ) / 𝑒 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑙 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 ↔ ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )
29 df-frgr ⊢ FriendGraph = { 𝑔 ∈ USGraph ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( Edg ‘ 𝑔 ) / 𝑒 ] ∀ 𝑘 ∈ 𝑣 ∀ 𝑙 ∈ ( 𝑣 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑣 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝑒 }
30 28 29 elrab2 ⊢ ( 𝐺 ∈ FriendGraph ↔ ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ 𝑉 ∀ 𝑙 ∈ ( 𝑉 ∖ { 𝑘 } ) ∃! 𝑥 ∈ 𝑉 { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ 𝐸 ) )