Metamath Proof Explorer

Theorem frcond3

Description: The friendship condition, expressed by neighborhoods: in a friendship graph, the neighborhood of a vertex and the neighborhood of a second, different vertex have exactly one vertex in common. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 30-Dec-2021)

Ref Expression
Hypotheses frcond1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
frcond1.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion frcond3 ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ∃ 𝑥 ∈ 𝑉 ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = { 𝑥 } ) )

Proof

Step Hyp Ref Expression
1 frcond1.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 frcond1.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 frcond1 ⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ∃! 𝑏 ∈ 𝑉 { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ) )
4 3 imp ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) → ∃! 𝑏 ∈ 𝑉 { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 )
5 ssrab2 ⊢ { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } ⊆ 𝑉
6 sseq1 ⊢ ( { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } = { 𝑥 } → ( { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } ⊆ 𝑉 ↔ { 𝑥 } ⊆ 𝑉 ) )
7 5 6 mpbii ⊢ ( { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } = { 𝑥 } → { 𝑥 } ⊆ 𝑉 )
8 vex ⊢ 𝑥 ∈ V
9 8 snss ⊢ ( 𝑥 ∈ 𝑉 ↔ { 𝑥 } ⊆ 𝑉 )
10 7 9 sylibr ⊢ ( { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } = { 𝑥 } → 𝑥 ∈ 𝑉 )
11 10 adantl ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) ∧ { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } = { 𝑥 } ) → 𝑥 ∈ 𝑉 )
12 frgrusgr ⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
13 1 2 nbusgr ⊢ ( 𝐺 ∈ USGraph → ( 𝐺 NeighbVtx 𝐴 ) = { 𝑏 ∈ 𝑉 ∣ { 𝐴 , 𝑏 } ∈ 𝐸 } )
14 1 2 nbusgr ⊢ ( 𝐺 ∈ USGraph → ( 𝐺 NeighbVtx 𝐶 ) = { 𝑏 ∈ 𝑉 ∣ { 𝐶 , 𝑏 } ∈ 𝐸 } )
15 13 14 ineq12d ⊢ ( 𝐺 ∈ USGraph → ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = ( { 𝑏 ∈ 𝑉 ∣ { 𝐴 , 𝑏 } ∈ 𝐸 } ∩ { 𝑏 ∈ 𝑉 ∣ { 𝐶 , 𝑏 } ∈ 𝐸 } ) )
16 12 15 syl ⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = ( { 𝑏 ∈ 𝑉 ∣ { 𝐴 , 𝑏 } ∈ 𝐸 } ∩ { 𝑏 ∈ 𝑉 ∣ { 𝐶 , 𝑏 } ∈ 𝐸 } ) )
17 16 adantr ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) → ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = ( { 𝑏 ∈ 𝑉 ∣ { 𝐴 , 𝑏 } ∈ 𝐸 } ∩ { 𝑏 ∈ 𝑉 ∣ { 𝐶 , 𝑏 } ∈ 𝐸 } ) )
18 17 adantr ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) ∧ { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } = { 𝑥 } ) → ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = ( { 𝑏 ∈ 𝑉 ∣ { 𝐴 , 𝑏 } ∈ 𝐸 } ∩ { 𝑏 ∈ 𝑉 ∣ { 𝐶 , 𝑏 } ∈ 𝐸 } ) )
19 inrab ⊢ ( { 𝑏 ∈ 𝑉 ∣ { 𝐴 , 𝑏 } ∈ 𝐸 } ∩ { 𝑏 ∈ 𝑉 ∣ { 𝐶 , 𝑏 } ∈ 𝐸 } ) = { 𝑏 ∈ 𝑉 ∣ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝐶 , 𝑏 } ∈ 𝐸 ) }
20 18 19 eqtrdi ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) ∧ { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } = { 𝑥 } ) → ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = { 𝑏 ∈ 𝑉 ∣ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝐶 , 𝑏 } ∈ 𝐸 ) } )
21 prcom ⊢ { 𝐶 , 𝑏 } = { 𝑏 , 𝐶 }
22 21 eleq1i ⊢ ( { 𝐶 , 𝑏 } ∈ 𝐸 ↔ { 𝑏 , 𝐶 } ∈ 𝐸 )
23 22 anbi2i ⊢ ( ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝐶 , 𝑏 } ∈ 𝐸 ) ↔ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) )
24 prex ⊢ { 𝐴 , 𝑏 } ∈ V
25 prex ⊢ { 𝑏 , 𝐶 } ∈ V
26 24 25 prss ⊢ ( ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝐶 } ∈ 𝐸 ) ↔ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 )
27 23 26 bitri ⊢ ( ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝐶 , 𝑏 } ∈ 𝐸 ) ↔ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 )
28 27 a1i ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) ∧ 𝑏 ∈ 𝑉 ) → ( ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝐶 , 𝑏 } ∈ 𝐸 ) ↔ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ) )
29 28 rabbidva ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) → { 𝑏 ∈ 𝑉 ∣ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝐶 , 𝑏 } ∈ 𝐸 ) } = { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } )
30 29 adantr ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) ∧ { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } = { 𝑥 } ) → { 𝑏 ∈ 𝑉 ∣ ( { 𝐴 , 𝑏 } ∈ 𝐸 ∧ { 𝐶 , 𝑏 } ∈ 𝐸 ) } = { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } )
31 simpr ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) ∧ { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } = { 𝑥 } ) → { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } = { 𝑥 } )
32 20 30 31 3eqtrd ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) ∧ { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } = { 𝑥 } ) → ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = { 𝑥 } )
33 11 32 jca ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) ∧ { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } = { 𝑥 } ) → ( 𝑥 ∈ 𝑉 ∧ ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = { 𝑥 } ) )
34 33 ex ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) → ( { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } = { 𝑥 } → ( 𝑥 ∈ 𝑉 ∧ ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = { 𝑥 } ) ) )
35 34 eximdv ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) → ( ∃ 𝑥 { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } = { 𝑥 } → ∃ 𝑥 ( 𝑥 ∈ 𝑉 ∧ ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = { 𝑥 } ) ) )
36 reusn ⊢ ( ∃! 𝑏 ∈ 𝑉 { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 ↔ ∃ 𝑥 { 𝑏 ∈ 𝑉 ∣ { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 } = { 𝑥 } )
37 df-rex ⊢ ( ∃ 𝑥 ∈ 𝑉 ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = { 𝑥 } ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑉 ∧ ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = { 𝑥 } ) )
38 35 36 37 3imtr4g ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) → ( ∃! 𝑏 ∈ 𝑉 { { 𝐴 , 𝑏 } , { 𝑏 , 𝐶 } } ⊆ 𝐸 → ∃ 𝑥 ∈ 𝑉 ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = { 𝑥 } ) )
39 4 38 mpd ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ) → ∃ 𝑥 ∈ 𝑉 ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = { 𝑥 } )
40 39 ex ⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ∃ 𝑥 ∈ 𝑉 ( ( 𝐺 NeighbVtx 𝐴 ) ∩ ( 𝐺 NeighbVtx 𝐶 ) ) = { 𝑥 } ) )