Proof of Theorem frgrwopreglem5
Step | Hyp | Ref
| Expression |
1 | | simpllr 776 |
. . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑎 ≠ 𝑥) |
2 | 1 | anim1i 618 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) |
3 | | simplll 775 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺 ∈ FriendGraph ) |
4 | | fveqeq2 6686 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑎 → ((𝐷‘𝑥) = 𝐾 ↔ (𝐷‘𝑎) = 𝐾)) |
5 | | frgrwopreg.a |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} |
6 | 4, 5 | elrab2 3592 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ 𝐴 ↔ (𝑎 ∈ 𝑉 ∧ (𝐷‘𝑎) = 𝐾)) |
7 | 6 | simplbi 501 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ 𝐴 → 𝑎 ∈ 𝑉) |
8 | | rabidim1 3284 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} → 𝑥 ∈ 𝑉) |
9 | 8, 5 | eleq2s 2852 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑉) |
10 | 7, 9 | anim12i 616 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) |
11 | 10 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) |
12 | | eldifi 4018 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ (𝑉 ∖ 𝐴) → 𝑏 ∈ 𝑉) |
13 | | frgrwopreg.b |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐵 = (𝑉 ∖ 𝐴) |
14 | 12, 13 | eleq2s 2852 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝐵 → 𝑏 ∈ 𝑉) |
15 | | eldifi 4018 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (𝑉 ∖ 𝐴) → 𝑦 ∈ 𝑉) |
16 | 15, 13 | eleq2s 2852 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑉) |
17 | 14, 16 | anim12i 616 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) |
18 | 11, 17 | anim12i 616 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))) |
19 | | frgrwopreg.v |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑉 = (Vtx‘𝐺) |
20 | | frgrwopreg.d |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = (VtxDeg‘𝐺) |
21 | | frgrwopreg.e |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐸 = (Edg‘𝐺) |
22 | 19, 20, 5, 13, 21 | frgrwopreglem5lem 28260 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐷‘𝑎) = (𝐷‘𝑥) ∧ (𝐷‘𝑎) ≠ (𝐷‘𝑏) ∧ (𝐷‘𝑥) ≠ (𝐷‘𝑦))) |
23 | 22 | adantll 714 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐷‘𝑎) = (𝐷‘𝑥) ∧ (𝐷‘𝑎) ≠ (𝐷‘𝑏) ∧ (𝐷‘𝑥) ≠ (𝐷‘𝑦))) |
24 | 3, 18, 23 | 3jca 1129 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐺 ∈ FriendGraph ∧ ((𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ((𝐷‘𝑎) = (𝐷‘𝑥) ∧ (𝐷‘𝑎) ≠ (𝐷‘𝑏) ∧ (𝐷‘𝑥) ≠ (𝐷‘𝑦)))) |
25 | 24 | adantr 484 |
. . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → (𝐺 ∈ FriendGraph ∧ ((𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ((𝐷‘𝑎) = (𝐷‘𝑥) ∧ (𝐷‘𝑎) ≠ (𝐷‘𝑏) ∧ (𝐷‘𝑥) ≠ (𝐷‘𝑦)))) |
26 | 19, 20, 21 | frgrwopreglem5a 28251 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FriendGraph ∧
((𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ((𝐷‘𝑎) = (𝐷‘𝑥) ∧ (𝐷‘𝑎) ≠ (𝐷‘𝑏) ∧ (𝐷‘𝑥) ≠ (𝐷‘𝑦))) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |
28 | | 3anass 1096 |
. . . . . . . . . . . . 13
⊢ (((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)) ↔ ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) |
29 | 2, 27, 28 | sylanbrc 586 |
. . . . . . . . . . . 12
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |
30 | 29 | ex 416 |
. . . . . . . . . . 11
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ≠ 𝑦 → ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) |
31 | 30 | reximdvva 3188 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) |
32 | 31 | exp31 423 |
. . . . . . . . 9
⊢ (𝐺 ∈ FriendGraph →
(𝑎 ≠ 𝑥 → ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))))) |
33 | 32 | com24 95 |
. . . . . . . 8
⊢ (𝐺 ∈ FriendGraph →
(∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑎 ≠ 𝑥 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))))) |
34 | 33 | imp31 421 |
. . . . . . 7
⊢ (((𝐺 ∈ FriendGraph ∧
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑎 ≠ 𝑥 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) |
35 | 34 | reximdvva 3188 |
. . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) → (∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) |
36 | 35 | ex 416 |
. . . . 5
⊢ (𝐺 ∈ FriendGraph →
(∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → (∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))))) |
37 | 36 | com13 88 |
. . . 4
⊢
(∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → (𝐺 ∈ FriendGraph → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))))) |
38 | 37 | imp 410 |
. . 3
⊢
((∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ∧ ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) → (𝐺 ∈ FriendGraph → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) |
39 | 19, 20, 5, 13 | frgrwopreglem1 28252 |
. . . 4
⊢ (𝐴 ∈ V ∧ 𝐵 ∈ V) |
40 | | hashgt12el 13878 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ 1 <
(♯‘𝐴)) →
∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥) |
41 | 40 | ex 416 |
. . . . 5
⊢ (𝐴 ∈ V → (1 <
(♯‘𝐴) →
∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥)) |
42 | | hashgt12el 13878 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ 1 <
(♯‘𝐵)) →
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) |
43 | 42 | ex 416 |
. . . . 5
⊢ (𝐵 ∈ V → (1 <
(♯‘𝐵) →
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦)) |
44 | 41, 43 | im2anan9 623 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((1 <
(♯‘𝐴) ∧ 1
< (♯‘𝐵))
→ (∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ∧ ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦))) |
45 | 39, 44 | ax-mp 5 |
. . 3
⊢ ((1 <
(♯‘𝐴) ∧ 1
< (♯‘𝐵))
→ (∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ∧ ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦)) |
46 | 38, 45 | syl11 33 |
. 2
⊢ (𝐺 ∈ FriendGraph → ((1
< (♯‘𝐴)
∧ 1 < (♯‘𝐵)) → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) |
47 | 46 | 3impib 1117 |
1
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝐴) ∧ 1
< (♯‘𝐵))
→ ∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |