Step | Hyp | Ref
| Expression |
1 | | simpllr 773 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑎 ≠ 𝑥) |
2 | 1 | anim1i 615 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) |
3 | | frgrwopreg.v |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑉 = (Vtx‘𝐺) |
4 | | frgrwopreg.d |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = (VtxDeg‘𝐺) |
5 | | frgrwopreg.a |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} |
6 | | frgrwopreg.b |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐵 = (𝑉 ∖ 𝐴) |
7 | | frgrwopreg.e |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐸 = (Edg‘𝐺) |
8 | 3, 4, 5, 6, 7 | frgrwopreglem4 28676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ FriendGraph →
∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸) |
9 | | preq1 4671 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑎 → {𝑧, 𝑏} = {𝑎, 𝑏}) |
10 | 9 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 𝑎 → ({𝑧, 𝑏} ∈ 𝐸 ↔ {𝑎, 𝑏} ∈ 𝐸)) |
11 | 10 | ralbidv 3119 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑎 → (∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ↔ ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ 𝐸)) |
12 | 11 | cbvralvw 3382 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ 𝐸) |
13 | | rsp2 3138 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑎 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ 𝐸 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → {𝑎, 𝑏} ∈ 𝐸)) |
14 | 13 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ 𝐸 → {𝑎, 𝑏} ∈ 𝐸)) |
15 | 14 | ad2ant2r 744 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ 𝐸 → {𝑎, 𝑏} ∈ 𝐸)) |
16 | 12, 15 | syl5bi 241 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → {𝑎, 𝑏} ∈ 𝐸)) |
17 | 16 | imp 407 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸) → {𝑎, 𝑏} ∈ 𝐸) |
18 | | prcom 4670 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑏, 𝑥} = {𝑥, 𝑏} |
19 | | preq1 4671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = 𝑥 → {𝑧, 𝑏} = {𝑥, 𝑏}) |
20 | 19 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = 𝑥 → ({𝑧, 𝑏} ∈ 𝐸 ↔ {𝑥, 𝑏} ∈ 𝐸)) |
21 | 20 | ralbidv 3119 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑥 → (∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ↔ ∀𝑏 ∈ 𝐵 {𝑥, 𝑏} ∈ 𝐸)) |
22 | 21 | cbvralvw 3382 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ↔ ∀𝑥 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑥, 𝑏} ∈ 𝐸) |
23 | | rsp2 3138 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑥 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑥, 𝑏} ∈ 𝐸 → ((𝑥 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → {𝑥, 𝑏} ∈ 𝐸)) |
24 | 22, 23 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → ((𝑥 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → {𝑥, 𝑏} ∈ 𝐸)) |
25 | 24 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → {𝑥, 𝑏} ∈ 𝐸)) |
26 | 25 | ad2ant2lr 745 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → {𝑥, 𝑏} ∈ 𝐸)) |
27 | 26 | imp 407 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸) → {𝑥, 𝑏} ∈ 𝐸) |
28 | 18, 27 | eqeltrid 2843 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸) → {𝑏, 𝑥} ∈ 𝐸) |
29 | 17, 28 | jca 512 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸)) |
30 | 29 | expcom 414 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸))) |
31 | 8, 30 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ FriendGraph →
(((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸))) |
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) → (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸))) |
33 | 32 | impl 456 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸)) |
34 | 33 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸)) |
35 | | preq2 4672 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 = 𝑦 → {𝑥, 𝑏} = {𝑥, 𝑦}) |
36 | 35 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = 𝑦 → ({𝑥, 𝑏} ∈ 𝐸 ↔ {𝑥, 𝑦} ∈ 𝐸)) |
37 | 20, 36 | rspc2v 3571 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → {𝑥, 𝑦} ∈ 𝐸)) |
38 | 37 | ad2ant2l 743 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → {𝑥, 𝑦} ∈ 𝐸)) |
39 | 38 | impcom 408 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ∧ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → {𝑥, 𝑦} ∈ 𝐸) |
40 | | prcom 4670 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑦, 𝑎} = {𝑎, 𝑦} |
41 | | preq2 4672 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 = 𝑦 → {𝑎, 𝑏} = {𝑎, 𝑦}) |
42 | 41 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 = 𝑦 → ({𝑎, 𝑏} ∈ 𝐸 ↔ {𝑎, 𝑦} ∈ 𝐸)) |
43 | 10, 42 | rspc2v 3571 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → {𝑎, 𝑦} ∈ 𝐸)) |
44 | 43 | ad2ant2rl 746 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → {𝑎, 𝑦} ∈ 𝐸)) |
45 | 44 | impcom 408 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ∧ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → {𝑎, 𝑦} ∈ 𝐸) |
46 | 40, 45 | eqeltrid 2843 |
. . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ∧ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → {𝑦, 𝑎} ∈ 𝐸) |
47 | 39, 46 | jca 512 |
. . . . . . . . . . . . . . . . . 18
⊢
((∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ∧ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)) |
48 | 47 | ex 413 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |
49 | 8, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ FriendGraph →
(((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |
50 | 49 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) → (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |
51 | 50 | impl 456 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)) |
52 | 51 | adantr 481 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)) |
53 | 2, 34, 52 | 3jca 1127 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |
54 | 53 | ex 413 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ≠ 𝑦 → ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) |
55 | 54 | reximdvva 3205 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) |
56 | 55 | exp31 420 |
. . . . . . . . 9
⊢ (𝐺 ∈ FriendGraph →
(𝑎 ≠ 𝑥 → ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))))) |
57 | 56 | com24 95 |
. . . . . . . 8
⊢ (𝐺 ∈ FriendGraph →
(∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑎 ≠ 𝑥 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))))) |
58 | 57 | imp31 418 |
. . . . . . 7
⊢ (((𝐺 ∈ FriendGraph ∧
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑎 ≠ 𝑥 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) |
59 | 58 | reximdvva 3205 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) → (∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) |
60 | 59 | ex 413 |
. . . . 5
⊢ (𝐺 ∈ FriendGraph →
(∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → (∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))))) |
61 | 60 | com13 88 |
. . . 4
⊢
(∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → (𝐺 ∈ FriendGraph → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))))) |
62 | 61 | imp 407 |
. . 3
⊢
((∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ∧ ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) → (𝐺 ∈ FriendGraph → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) |
63 | 3, 4, 5, 6 | frgrwopreglem1 28673 |
. . . 4
⊢ (𝐴 ∈ V ∧ 𝐵 ∈ V) |
64 | | hashgt12el 14135 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 1 <
(♯‘𝐴)) →
∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥) |
65 | 64 | ex 413 |
. . . . 5
⊢ (𝐴 ∈ V → (1 <
(♯‘𝐴) →
∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥)) |
66 | | hashgt12el 14135 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ 1 <
(♯‘𝐵)) →
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) |
67 | 66 | ex 413 |
. . . . 5
⊢ (𝐵 ∈ V → (1 <
(♯‘𝐵) →
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦)) |
68 | 65, 67 | im2anan9 620 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((1 <
(♯‘𝐴) ∧ 1
< (♯‘𝐵))
→ (∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ∧ ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦))) |
69 | 63, 68 | ax-mp 5 |
. . 3
⊢ ((1 <
(♯‘𝐴) ∧ 1
< (♯‘𝐵))
→ (∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ∧ ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦)) |
70 | 62, 69 | syl11 33 |
. 2
⊢ (𝐺 ∈ FriendGraph → ((1
< (♯‘𝐴)
∧ 1 < (♯‘𝐵)) → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) |
71 | 70 | 3impib 1115 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝐴) ∧ 1
< (♯‘𝐵))
→ ∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |