Metamath Proof Explorer

Theorem frgrwopreglem5

Description: Lemma 5 for frgrwopreg . If A as well as B contain at least two vertices, there is a 4-cycle in a friendship graph. This corresponds to statement 6 in Huneke p. 2: "... otherwise, there are two different vertices in A, and they have two common neighbors in B, ...". (Contributed by Alexander van der Vekens, 31-Dec-2017) (Proof shortened by AV, 5-Feb-2022)

Ref Expression
Hypotheses frgrwopreg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
frgrwopreg.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
frgrwopreg.a ⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
frgrwopreg.b ⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
frgrwopreg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion frgrwopreglem5 ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝐴 ) ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 frgrwopreg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 frgrwopreg.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
3 frgrwopreg.a ⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
4 frgrwopreg.b ⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
5 frgrwopreg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
6 simpllr ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑎 ≠ 𝑥 )
7 6 anim1i ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑏 ≠ 𝑦 ) → ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) )
8 simplll ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐺 ∈ FriendGraph )
9 fveqeq2 ⊢ ( 𝑥 = 𝑎 → ( ( 𝐷 ‘ 𝑥 ) = 𝐾 ↔ ( 𝐷 ‘ 𝑎 ) = 𝐾 ) )
10 9 3 elrab2 ⊢ ( 𝑎 ∈ 𝐴 ↔ ( 𝑎 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑎 ) = 𝐾 ) )
11 10 simplbi ⊢ ( 𝑎 ∈ 𝐴 → 𝑎 ∈ 𝑉 )
12 rabidim1 ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 } → 𝑥 ∈ 𝑉 )
13 12 3 eleq2s ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑉 )
14 11 13 anim12i ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) )
15 14 adantl ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) )
16 eldifi ⊢ ( 𝑏 ∈ ( 𝑉 ∖ 𝐴 ) → 𝑏 ∈ 𝑉 )
17 16 4 eleq2s ⊢ ( 𝑏 ∈ 𝐵 → 𝑏 ∈ 𝑉 )
18 eldifi ⊢ ( 𝑦 ∈ ( 𝑉 ∖ 𝐴 ) → 𝑦 ∈ 𝑉 )
19 18 4 eleq2s ⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑉 )
20 17 19 anim12i ⊢ ( ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) )
21 15 20 anim12i ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
22 1 2 3 4 5 frgrwopreglem5lem ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) ∧ ( 𝐷 ‘ 𝑎 ) ≠ ( 𝐷 ‘ 𝑏 ) ∧ ( 𝐷 ‘ 𝑥 ) ≠ ( 𝐷 ‘ 𝑦 ) ) )
23 22 adantll ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) ∧ ( 𝐷 ‘ 𝑎 ) ≠ ( 𝐷 ‘ 𝑏 ) ∧ ( 𝐷 ‘ 𝑥 ) ≠ ( 𝐷 ‘ 𝑦 ) ) )
24 8 21 23 3jca ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐺 ∈ FriendGraph ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) ∧ ( 𝐷 ‘ 𝑎 ) ≠ ( 𝐷 ‘ 𝑏 ) ∧ ( 𝐷 ‘ 𝑥 ) ≠ ( 𝐷 ‘ 𝑦 ) ) ) )
25 24 adantr ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑏 ≠ 𝑦 ) → ( 𝐺 ∈ FriendGraph ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) ∧ ( 𝐷 ‘ 𝑎 ) ≠ ( 𝐷 ‘ 𝑏 ) ∧ ( 𝐷 ‘ 𝑥 ) ≠ ( 𝐷 ‘ 𝑦 ) ) ) )
26 1 2 5 frgrwopreglem5a ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( ( 𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( ( 𝐷 ‘ 𝑎 ) = ( 𝐷 ‘ 𝑥 ) ∧ ( 𝐷 ‘ 𝑎 ) ≠ ( 𝐷 ‘ 𝑏 ) ∧ ( 𝐷 ‘ 𝑥 ) ≠ ( 𝐷 ‘ 𝑦 ) ) ) → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) )
27 25 26 syl ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑏 ≠ 𝑦 ) → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) )
28 3anass ⊢ ( ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ↔ ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) )
29 7 27 28 sylanbrc ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑏 ≠ 𝑦 ) → ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) )
30 29 ex ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑏 ≠ 𝑦 → ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) )
31 30 reximdvva ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) )
32 31 exp31 ⊢ ( 𝐺 ∈ FriendGraph → ( 𝑎 ≠ 𝑥 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) ) ) )
33 32 com24 ⊢ ( 𝐺 ∈ FriendGraph → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑎 ≠ 𝑥 → ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) ) ) )
34 33 imp31 ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑎 ≠ 𝑥 → ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) )
35 34 reximdvva ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) )
36 35 ex ⊢ ( 𝐺 ∈ FriendGraph → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) ) )
37 36 com13 ⊢ ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ( 𝐺 ∈ FriendGraph → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) ) )
38 37 imp ⊢ ( ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ∧ ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) )
39 1 2 3 4 frgrwopreglem1 ⊢ ( 𝐴 ∈ V ∧ 𝐵 ∈ V )
40 hashgt12el ⊢ ( ( 𝐴 ∈ V ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 )
41 40 ex ⊢ ( 𝐴 ∈ V → ( 1 < ( ♯ ‘ 𝐴 ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ) )
42 hashgt12el ⊢ ( ( 𝐵 ∈ V ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 )
43 42 ex ⊢ ( 𝐵 ∈ V → ( 1 < ( ♯ ‘ 𝐵 ) → ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 ) )
44 41 43 im2anan9 ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 1 < ( ♯ ‘ 𝐴 ) ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ∧ ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 ) ) )
45 39 44 ax-mp ⊢ ( ( 1 < ( ♯ ‘ 𝐴 ) ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ∧ ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 ) )
46 38 45 syl11 ⊢ ( 𝐺 ∈ FriendGraph → ( ( 1 < ( ♯ ‘ 𝐴 ) ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) )
47 46 3impib ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝐴 ) ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) )