Proof of Theorem frgrwopreglem5
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpllr 775 | . . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑎 ≠ 𝑥) | 
| 2 | 1 | anim1i 615 | . . . . . . . . . . . . 13
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → (𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦)) | 
| 3 |  | simplll 774 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐺 ∈ FriendGraph ) | 
| 4 |  | fveqeq2 6914 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑎 → ((𝐷‘𝑥) = 𝐾 ↔ (𝐷‘𝑎) = 𝐾)) | 
| 5 |  | frgrwopreg.a | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} | 
| 6 | 4, 5 | elrab2 3694 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ 𝐴 ↔ (𝑎 ∈ 𝑉 ∧ (𝐷‘𝑎) = 𝐾)) | 
| 7 | 6 | simplbi 497 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 ∈ 𝐴 → 𝑎 ∈ 𝑉) | 
| 8 |  | rabidim1 3458 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾} → 𝑥 ∈ 𝑉) | 
| 9 | 8, 5 | eleq2s 2858 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝑉) | 
| 10 | 7, 9 | anim12i 613 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) | 
| 11 | 10 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉)) | 
| 12 |  | eldifi 4130 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 ∈ (𝑉 ∖ 𝐴) → 𝑏 ∈ 𝑉) | 
| 13 |  | frgrwopreg.b | . . . . . . . . . . . . . . . . . . 19
⊢ 𝐵 = (𝑉 ∖ 𝐴) | 
| 14 | 12, 13 | eleq2s 2858 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ 𝐵 → 𝑏 ∈ 𝑉) | 
| 15 |  | eldifi 4130 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ (𝑉 ∖ 𝐴) → 𝑦 ∈ 𝑉) | 
| 16 | 15, 13 | eleq2s 2858 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑉) | 
| 17 | 14, 16 | anim12i 613 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) | 
| 18 | 11, 17 | anim12i 613 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉))) | 
| 19 |  | frgrwopreg.v | . . . . . . . . . . . . . . . . . 18
⊢ 𝑉 = (Vtx‘𝐺) | 
| 20 |  | frgrwopreg.d | . . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = (VtxDeg‘𝐺) | 
| 21 |  | frgrwopreg.e | . . . . . . . . . . . . . . . . . 18
⊢ 𝐸 = (Edg‘𝐺) | 
| 22 | 19, 20, 5, 13, 21 | frgrwopreglem5lem 30340 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐷‘𝑎) = (𝐷‘𝑥) ∧ (𝐷‘𝑎) ≠ (𝐷‘𝑏) ∧ (𝐷‘𝑥) ≠ (𝐷‘𝑦))) | 
| 23 | 22 | adantll 714 | . . . . . . . . . . . . . . . 16
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐷‘𝑎) = (𝐷‘𝑥) ∧ (𝐷‘𝑎) ≠ (𝐷‘𝑏) ∧ (𝐷‘𝑥) ≠ (𝐷‘𝑦))) | 
| 24 | 3, 18, 23 | 3jca 1128 | . . . . . . . . . . . . . . 15
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐺 ∈ FriendGraph ∧ ((𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ((𝐷‘𝑎) = (𝐷‘𝑥) ∧ (𝐷‘𝑎) ≠ (𝐷‘𝑏) ∧ (𝐷‘𝑥) ≠ (𝐷‘𝑦)))) | 
| 25 | 24 | adantr 480 | . . . . . . . . . . . . . 14
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → (𝐺 ∈ FriendGraph ∧ ((𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ((𝐷‘𝑎) = (𝐷‘𝑥) ∧ (𝐷‘𝑎) ≠ (𝐷‘𝑏) ∧ (𝐷‘𝑥) ≠ (𝐷‘𝑦)))) | 
| 26 | 19, 20, 21 | frgrwopreglem5a 30331 | . . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ FriendGraph ∧
((𝑎 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) ∧ (𝑏 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ ((𝐷‘𝑎) = (𝐷‘𝑥) ∧ (𝐷‘𝑎) ≠ (𝐷‘𝑏) ∧ (𝐷‘𝑥) ≠ (𝐷‘𝑦))) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) | 
| 27 | 25, 26 | syl 17 | . . . . . . . . . . . . 13
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) | 
| 28 |  | 3anass 1094 | . . . . . . . . . . . . 13
⊢ (((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)) ↔ ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) | 
| 29 | 2, 27, 28 | sylanbrc 583 | . . . . . . . . . . . 12
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) | 
| 30 | 29 | ex 412 | . . . . . . . . . . 11
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ≠ 𝑦 → ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) | 
| 31 | 30 | reximdvva 3206 | . . . . . . . . . 10
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) | 
| 32 | 31 | exp31 419 | . . . . . . . . 9
⊢ (𝐺 ∈ FriendGraph →
(𝑎 ≠ 𝑥 → ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))))) | 
| 33 | 32 | com24 95 | . . . . . . . 8
⊢ (𝐺 ∈ FriendGraph →
(∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑎 ≠ 𝑥 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))))) | 
| 34 | 33 | imp31 417 | . . . . . . 7
⊢ (((𝐺 ∈ FriendGraph ∧
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑎 ≠ 𝑥 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) | 
| 35 | 34 | reximdvva 3206 | . . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) → (∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) | 
| 36 | 35 | ex 412 | . . . . 5
⊢ (𝐺 ∈ FriendGraph →
(∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → (∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))))) | 
| 37 | 36 | com13 88 | . . . 4
⊢
(∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → (𝐺 ∈ FriendGraph → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))))) | 
| 38 | 37 | imp 406 | . . 3
⊢
((∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ∧ ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) → (𝐺 ∈ FriendGraph → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) | 
| 39 | 19, 20, 5, 13 | frgrwopreglem1 30332 | . . . 4
⊢ (𝐴 ∈ V ∧ 𝐵 ∈ V) | 
| 40 |  | hashgt12el 14462 | . . . . . 6
⊢ ((𝐴 ∈ V ∧ 1 <
(♯‘𝐴)) →
∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥) | 
| 41 | 40 | ex 412 | . . . . 5
⊢ (𝐴 ∈ V → (1 <
(♯‘𝐴) →
∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥)) | 
| 42 |  | hashgt12el 14462 | . . . . . 6
⊢ ((𝐵 ∈ V ∧ 1 <
(♯‘𝐵)) →
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) | 
| 43 | 42 | ex 412 | . . . . 5
⊢ (𝐵 ∈ V → (1 <
(♯‘𝐵) →
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦)) | 
| 44 | 41, 43 | im2anan9 620 | . . . 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 1116 | 1
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝐴) ∧ 1
< (♯‘𝐵))
→ ∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |