Metamath Proof Explorer

Theorem frgrwopreglem5ALT

Description: Alternate direct proof of frgrwopreglem5 , not using frgrwopreglem5a . This proof would be even a little bit shorter than the proof of frgrwopreglem5 without using frgrwopreglem5lem . (Contributed by Alexander van der Vekens, 31-Dec-2017) (Revised by AV, 3-Jan-2022) (Proof shortened by AV, 5-Feb-2022) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses frgrwopreg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
frgrwopreg.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
frgrwopreg.a ⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
frgrwopreg.b ⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
frgrwopreg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion frgrwopreglem5ALT ( ( 𝐺 ∈ 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 1 2 3 4 5 frgrwopreglem4 ⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 )
9 preq1 ⊢ ( 𝑧 = 𝑎 → { 𝑧 , 𝑏 } = { 𝑎 , 𝑏 } )
10 9 eleq1d ⊢ ( 𝑧 = 𝑎 → ( { 𝑧 , 𝑏 } ∈ 𝐸 ↔ { 𝑎 , 𝑏 } ∈ 𝐸 ) )
11 10 ralbidv ⊢ ( 𝑧 = 𝑎 → ( ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 ↔ ∀ 𝑏 ∈ 𝐵 { 𝑎 , 𝑏 } ∈ 𝐸 ) )
12 11 cbvralvw ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑎 , 𝑏 } ∈ 𝐸 )
13 rsp2 ⊢ ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑎 , 𝑏 } ∈ 𝐸 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
14 13 com12 ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑎 , 𝑏 } ∈ 𝐸 → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
15 14 ad2ant2r ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑎 , 𝑏 } ∈ 𝐸 → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
16 12 15 biimtrid ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
17 16 imp ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 ) → { 𝑎 , 𝑏 } ∈ 𝐸 )
18 prcom ⊢ { 𝑏 , 𝑥 } = { 𝑥 , 𝑏 }
19 preq1 ⊢ ( 𝑧 = 𝑥 → { 𝑧 , 𝑏 } = { 𝑥 , 𝑏 } )
20 19 eleq1d ⊢ ( 𝑧 = 𝑥 → ( { 𝑧 , 𝑏 } ∈ 𝐸 ↔ { 𝑥 , 𝑏 } ∈ 𝐸 ) )
21 20 ralbidv ⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 ↔ ∀ 𝑏 ∈ 𝐵 { 𝑥 , 𝑏 } ∈ 𝐸 ) )
22 21 cbvralvw ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑥 , 𝑏 } ∈ 𝐸 )
23 rsp2 ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑥 , 𝑏 } ∈ 𝐸 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → { 𝑥 , 𝑏 } ∈ 𝐸 ) )
24 22 23 sylbi ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → { 𝑥 , 𝑏 } ∈ 𝐸 ) )
25 24 com12 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 → { 𝑥 , 𝑏 } ∈ 𝐸 ) )
26 25 ad2ant2lr ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 → { 𝑥 , 𝑏 } ∈ 𝐸 ) )
27 26 imp ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 ) → { 𝑥 , 𝑏 } ∈ 𝐸 )
28 18 27 eqeltrid ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 ) → { 𝑏 , 𝑥 } ∈ 𝐸 )
29 17 28 jca ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) )
30 29 expcom ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ) )
31 8 30 syl ⊢ ( 𝐺 ∈ FriendGraph → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ) )
32 31 adantr ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ) )
33 32 impl ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) )
34 33 adantr ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑏 ≠ 𝑦 ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) )
35 preq2 ⊢ ( 𝑏 = 𝑦 → { 𝑥 , 𝑏 } = { 𝑥 , 𝑦 } )
36 35 eleq1d ⊢ ( 𝑏 = 𝑦 → ( { 𝑥 , 𝑏 } ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
37 20 36 rspc2v ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 → { 𝑥 , 𝑦 } ∈ 𝐸 ) )
38 37 ad2ant2l ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 → { 𝑥 , 𝑦 } ∈ 𝐸 ) )
39 38 impcom ⊢ ( ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → { 𝑥 , 𝑦 } ∈ 𝐸 )
40 prcom ⊢ { 𝑦 , 𝑎 } = { 𝑎 , 𝑦 }
41 preq2 ⊢ ( 𝑏 = 𝑦 → { 𝑎 , 𝑏 } = { 𝑎 , 𝑦 } )
42 41 eleq1d ⊢ ( 𝑏 = 𝑦 → ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { 𝑎 , 𝑦 } ∈ 𝐸 ) )
43 10 42 rspc2v ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 → { 𝑎 , 𝑦 } ∈ 𝐸 ) )
44 43 ad2ant2rl ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 → { 𝑎 , 𝑦 } ∈ 𝐸 ) )
45 44 impcom ⊢ ( ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → { 𝑎 , 𝑦 } ∈ 𝐸 )
46 40 45 eqeltrid ⊢ ( ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → { 𝑦 , 𝑎 } ∈ 𝐸 )
47 39 46 jca ⊢ ( ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) )
48 47 ex ⊢ ( ∀ 𝑧 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 { 𝑧 , 𝑏 } ∈ 𝐸 → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) )
49 8 48 syl ⊢ ( 𝐺 ∈ FriendGraph → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) )
50 49 adantr ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) )
51 50 impl ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) )
52 51 adantr ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑏 ≠ 𝑦 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) )
53 7 34 52 3jca ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑏 ≠ 𝑦 ) → ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) )
54 53 ex ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑏 ≠ 𝑦 → ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) )
55 54 reximdvva ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) )
56 55 exp31 ⊢ ( 𝐺 ∈ FriendGraph → ( 𝑎 ≠ 𝑥 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) ) ) )
57 56 com24 ⊢ ( 𝐺 ∈ FriendGraph → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑎 ≠ 𝑥 → ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) ) ) )
58 57 imp31 ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → ( 𝑎 ≠ 𝑥 → ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) )
59 58 reximdvva ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) )
60 59 ex ⊢ ( 𝐺 ∈ FriendGraph → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) ) )
61 60 com13 ⊢ ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ( 𝐺 ∈ FriendGraph → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) ) )
62 61 imp ⊢ ( ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ∧ ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) )
63 1 2 3 4 frgrwopreglem1 ⊢ ( 𝐴 ∈ V ∧ 𝐵 ∈ V )
64 hashgt12el ⊢ ( ( 𝐴 ∈ V ∧ 1 < ( ♯ ‘ 𝐴 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 )
65 64 ex ⊢ ( 𝐴 ∈ V → ( 1 < ( ♯ ‘ 𝐴 ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ) )
66 hashgt12el ⊢ ( ( 𝐵 ∈ V ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 )
67 66 ex ⊢ ( 𝐵 ∈ V → ( 1 < ( ♯ ‘ 𝐵 ) → ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 ) )
68 65 67 im2anan9 ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 1 < ( ♯ ‘ 𝐴 ) ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ∧ ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 ) ) )
69 63 68 ax-mp ⊢ ( ( 1 < ( ♯ ‘ 𝐴 ) ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ∧ ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 ) )
70 62 69 syl11 ⊢ ( 𝐺 ∈ FriendGraph → ( ( 1 < ( ♯ ‘ 𝐴 ) ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) ) )
71 70 3impib ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝐴 ) ∧ 1 < ( ♯ ‘ 𝐵 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑦 ∈ 𝐵 ( ( 𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦 ) ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑥 } ∈ 𝐸 ) ∧ ( { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝑎 } ∈ 𝐸 ) ) )