Metamath Proof Explorer

Theorem n4cyclfrgr

Description: There is no 4-cycle in a friendship graph, see Proposition 1(a) of MertziosUnger p. 153 : "A friendship graph G contains no C4 as a subgraph ...". (Contributed by Alexander van der Vekens, 19-Nov-2017) (Revised by AV, 2-Apr-2021)

Ref Expression
Assertion n4cyclfrgr ( ( 𝐺 ∈ FriendGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) → ( ♯ ‘ 𝐹 ) ≠ 4 )

Proof

Step Hyp Ref Expression
1 frgrusgr ⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
2 usgrupgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UPGraph )
3 1 2 syl ⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ UPGraph )
4 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
6 4 5 upgr4cycl4dv4e ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 4 ) → ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) )
7 4 5 isfrgr ⊢ ( 𝐺 ∈ FriendGraph ↔ ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
8 simplrl ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → 𝑐 ∈ ( Vtx ‘ 𝐺 ) )
9 necom ⊢ ( 𝑎 ≠ 𝑐 ↔ 𝑐 ≠ 𝑎 )
10 9 biimpi ⊢ ( 𝑎 ≠ 𝑐 → 𝑐 ≠ 𝑎 )
11 10 3ad2ant2 ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) → 𝑐 ≠ 𝑎 )
12 11 ad2antrl ⊢ ( ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) → 𝑐 ≠ 𝑎 )
13 12 adantl ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → 𝑐 ≠ 𝑎 )
14 eldifsn ⊢ ( 𝑐 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑎 } ) ↔ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑐 ≠ 𝑎 ) )
15 8 13 14 sylanbrc ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → 𝑐 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑎 } ) )
16 sneq ⊢ ( 𝑘 = 𝑎 → { 𝑘 } = { 𝑎 } )
17 16 difeq2d ⊢ ( 𝑘 = 𝑎 → ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) = ( ( Vtx ‘ 𝐺 ) ∖ { 𝑎 } ) )
18 preq2 ⊢ ( 𝑘 = 𝑎 → { 𝑥 , 𝑘 } = { 𝑥 , 𝑎 } )
19 18 preq1d ⊢ ( 𝑘 = 𝑎 → { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } = { { 𝑥 , 𝑎 } , { 𝑥 , 𝑙 } } )
20 19 sseq1d ⊢ ( 𝑘 = 𝑎 → ( { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ { { 𝑥 , 𝑎 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
21 20 reubidv ⊢ ( 𝑘 = 𝑎 → ( ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑎 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
22 17 21 raleqbidv ⊢ ( 𝑘 = 𝑎 → ( ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑎 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑎 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
23 22 rspcv ⊢ ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) → ( ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) → ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑎 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑎 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
24 23 ad3antrrr ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) → ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑎 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑎 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) )
25 preq2 ⊢ ( 𝑙 = 𝑐 → { 𝑥 , 𝑙 } = { 𝑥 , 𝑐 } )
26 25 preq2d ⊢ ( 𝑙 = 𝑐 → { { 𝑥 , 𝑎 } , { 𝑥 , 𝑙 } } = { { 𝑥 , 𝑎 } , { 𝑥 , 𝑐 } } )
27 26 sseq1d ⊢ ( 𝑙 = 𝑐 → ( { { 𝑥 , 𝑎 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ { { 𝑥 , 𝑎 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) ) )
28 27 reubidv ⊢ ( 𝑙 = 𝑐 → ( ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑎 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ↔ ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑎 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) ) )
29 28 rspcv ⊢ ( 𝑐 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑎 } ) → ( ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑎 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑎 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) → ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑎 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) ) )
30 15 24 29 sylsyld ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) → ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑎 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) ) )
31 prcom ⊢ { 𝑥 , 𝑎 } = { 𝑎 , 𝑥 }
32 31 preq1i ⊢ { { 𝑥 , 𝑎 } , { 𝑥 , 𝑐 } } = { { 𝑎 , 𝑥 } , { 𝑥 , 𝑐 } }
33 32 sseq1i ⊢ ( { { 𝑥 , 𝑎 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) ↔ { { 𝑎 , 𝑥 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) )
34 33 reubii ⊢ ( ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑎 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) ↔ ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑎 , 𝑥 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) )
35 simprll ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) )
36 simprlr ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) )
37 simpllr ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → 𝑏 ∈ ( Vtx ‘ 𝐺 ) )
38 simplrr ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → 𝑑 ∈ ( Vtx ‘ 𝐺 ) )
39 simprr2 ⊢ ( ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) → 𝑏 ≠ 𝑑 )
40 39 adantl ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → 𝑏 ≠ 𝑑 )
41 4cycl2vnunb ⊢ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ≠ 𝑑 ) ) → ¬ ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑎 , 𝑥 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) )
42 35 36 37 38 40 41 syl113anc ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ¬ ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑎 , 𝑥 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) )
43 42 pm2.21d ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑎 , 𝑥 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) → ( ♯ ‘ 𝐹 ) ≠ 4 ) )
44 43 com12 ⊢ ( ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑎 , 𝑥 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) → ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( ♯ ‘ 𝐹 ) ≠ 4 ) )
45 34 44 sylbi ⊢ ( ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑎 } , { 𝑥 , 𝑐 } } ⊆ ( Edg ‘ 𝐺 ) → ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( ♯ ‘ 𝐹 ) ≠ 4 ) )
46 30 45 syl6 ⊢ ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) → ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( ♯ ‘ 𝐹 ) ≠ 4 ) ) )
47 46 pm2.43b ⊢ ( ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) → ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( ♯ ‘ 𝐹 ) ≠ 4 ) )
48 47 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑘 ∈ ( Vtx ‘ 𝐺 ) ∀ 𝑙 ∈ ( ( Vtx ‘ 𝐺 ) ∖ { 𝑘 } ) ∃! 𝑥 ∈ ( Vtx ‘ 𝐺 ) { { 𝑥 , 𝑘 } , { 𝑥 , 𝑙 } } ⊆ ( Edg ‘ 𝐺 ) ) → ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( ♯ ‘ 𝐹 ) ≠ 4 ) )
49 7 48 sylbi ⊢ ( 𝐺 ∈ FriendGraph → ( ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) ∧ ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) ) → ( ♯ ‘ 𝐹 ) ≠ 4 ) )
50 49 expdcom ⊢ ( ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) ∧ ( 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ) ) → ( ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) → ( 𝐺 ∈ FriendGraph → ( ♯ ‘ 𝐹 ) ≠ 4 ) ) )
51 50 rexlimdvva ⊢ ( ( 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ) → ( ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) → ( 𝐺 ∈ FriendGraph → ( ♯ ‘ 𝐹 ) ≠ 4 ) ) )
52 51 rexlimivv ⊢ ( ∃ 𝑎 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑏 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑐 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑑 ∈ ( Vtx ‘ 𝐺 ) ( ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( { 𝑐 , 𝑑 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑑 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ ( ( 𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑 ) ∧ ( 𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑 ) ) ) → ( 𝐺 ∈ FriendGraph → ( ♯ ‘ 𝐹 ) ≠ 4 ) )
53 6 52 syl ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ∧ ( ♯ ‘ 𝐹 ) = 4 ) → ( 𝐺 ∈ FriendGraph → ( ♯ ‘ 𝐹 ) ≠ 4 ) )
54 53 3exp ⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 4 → ( 𝐺 ∈ FriendGraph → ( ♯ ‘ 𝐹 ) ≠ 4 ) ) ) )
55 54 com34 ⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( 𝐺 ∈ FriendGraph → ( ( ♯ ‘ 𝐹 ) = 4 → ( ♯ ‘ 𝐹 ) ≠ 4 ) ) ) )
56 55 com23 ⊢ ( 𝐺 ∈ UPGraph → ( 𝐺 ∈ FriendGraph → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 4 → ( ♯ ‘ 𝐹 ) ≠ 4 ) ) ) )
57 3 56 mpcom ⊢ ( 𝐺 ∈ FriendGraph → ( 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 → ( ( ♯ ‘ 𝐹 ) = 4 → ( ♯ ‘ 𝐹 ) ≠ 4 ) ) )
58 57 imp ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) → ( ( ♯ ‘ 𝐹 ) = 4 → ( ♯ ‘ 𝐹 ) ≠ 4 ) )
59 neqne ⊢ ( ¬ ( ♯ ‘ 𝐹 ) = 4 → ( ♯ ‘ 𝐹 ) ≠ 4 )
60 58 59 pm2.61d1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝐹 ( Cycles ‘ 𝐺 ) 𝑃 ) → ( ♯ ‘ 𝐹 ) ≠ 4 )