Theorem 4cycl2v2nb

Description: In a (maybe degenerate) 4-cycle, two vertice have two (maybe not different) common neighbors. (Contributed by Alexander van der Vekens, 19-Nov-2017) (Revised by AV, 2-Apr-2021)

	Ref	Expression
Assertion	4cycl2v2nb	⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) ) → ( { { 𝐴 , 𝐵 } , { 𝐵 , 𝐶 } } ⊆ 𝐸 ∧ { { 𝐴 , 𝐷 } , { 𝐷 , 𝐶 } } ⊆ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		prssi	⊢ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) → { { 𝐴 , 𝐵 } , { 𝐵 , 𝐶 } } ⊆ 𝐸 )
2		prcom	⊢ { 𝐷 , 𝐴 } = { 𝐴 , 𝐷 }
3	2	eleq1i	⊢ ( { 𝐷 , 𝐴 } ∈ 𝐸 ↔ { 𝐴 , 𝐷 } ∈ 𝐸 )
4	3	biimpi	⊢ ( { 𝐷 , 𝐴 } ∈ 𝐸 → { 𝐴 , 𝐷 } ∈ 𝐸 )
5		prcom	⊢ { 𝐶 , 𝐷 } = { 𝐷 , 𝐶 }
6	5	eleq1i	⊢ ( { 𝐶 , 𝐷 } ∈ 𝐸 ↔ { 𝐷 , 𝐶 } ∈ 𝐸 )
7	6	biimpi	⊢ ( { 𝐶 , 𝐷 } ∈ 𝐸 → { 𝐷 , 𝐶 } ∈ 𝐸 )
8		prssi	⊢ ( ( { 𝐴 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐶 } ∈ 𝐸 ) → { { 𝐴 , 𝐷 } , { 𝐷 , 𝐶 } } ⊆ 𝐸 )
9	4 7 8	syl2anr	⊢ ( ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) → { { 𝐴 , 𝐷 } , { 𝐷 , 𝐶 } } ⊆ 𝐸 )
10	1 9	anim12i	⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) ) → ( { { 𝐴 , 𝐵 } , { 𝐵 , 𝐶 } } ⊆ 𝐸 ∧ { { 𝐴 , 𝐷 } , { 𝐷 , 𝐶 } } ⊆ 𝐸 ) )