| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpllr 775 | . . . . . . . . . . . . . 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 30335 | . . . . . . . . . . . . . . . . 17
⊢ (𝐺 ∈ FriendGraph →
∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸) | 
| 9 |  | preq1 4732 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 = 𝑎 → {𝑧, 𝑏} = {𝑎, 𝑏}) | 
| 10 | 9 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = 𝑎 → ({𝑧, 𝑏} ∈ 𝐸 ↔ {𝑎, 𝑏} ∈ 𝐸)) | 
| 11 | 10 | ralbidv 3177 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = 𝑎 → (∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ↔ ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ 𝐸)) | 
| 12 | 11 | cbvralvw 3236 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ 𝐸) | 
| 13 |  | rsp2 3276 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑎 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ 𝐸 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → {𝑎, 𝑏} ∈ 𝐸)) | 
| 14 | 13 | com12 32 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ 𝐸 → {𝑎, 𝑏} ∈ 𝐸)) | 
| 15 | 14 | ad2ant2r 747 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ 𝐸 → {𝑎, 𝑏} ∈ 𝐸)) | 
| 16 | 12, 15 | biimtrid 242 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → {𝑎, 𝑏} ∈ 𝐸)) | 
| 17 | 16 | imp 406 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸) → {𝑎, 𝑏} ∈ 𝐸) | 
| 18 |  | prcom 4731 | . . . . . . . . . . . . . . . . . . . 20
⊢ {𝑏, 𝑥} = {𝑥, 𝑏} | 
| 19 |  | preq1 4732 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑧 = 𝑥 → {𝑧, 𝑏} = {𝑥, 𝑏}) | 
| 20 | 19 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑧 = 𝑥 → ({𝑧, 𝑏} ∈ 𝐸 ↔ {𝑥, 𝑏} ∈ 𝐸)) | 
| 21 | 20 | ralbidv 3177 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 = 𝑥 → (∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ↔ ∀𝑏 ∈ 𝐵 {𝑥, 𝑏} ∈ 𝐸)) | 
| 22 | 21 | cbvralvw 3236 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ↔ ∀𝑥 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑥, 𝑏} ∈ 𝐸) | 
| 23 |  | rsp2 3276 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑥 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑥, 𝑏} ∈ 𝐸 → ((𝑥 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → {𝑥, 𝑏} ∈ 𝐸)) | 
| 24 | 22, 23 | sylbi 217 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → ((𝑥 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → {𝑥, 𝑏} ∈ 𝐸)) | 
| 25 | 24 | com12 32 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → {𝑥, 𝑏} ∈ 𝐸)) | 
| 26 | 25 | ad2ant2lr 748 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → {𝑥, 𝑏} ∈ 𝐸)) | 
| 27 | 26 | imp 406 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸) → {𝑥, 𝑏} ∈ 𝐸) | 
| 28 | 18, 27 | eqeltrid 2844 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸) → {𝑏, 𝑥} ∈ 𝐸) | 
| 29 | 17, 28 | jca 511 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ ∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸)) | 
| 30 | 29 | expcom 413 | . . . . . . . . . . . . . . . . 17
⊢
(∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸))) | 
| 31 | 8, 30 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ FriendGraph →
(((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸))) | 
| 32 | 31 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) → (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸))) | 
| 33 | 32 | impl 455 | . . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸)) | 
| 34 | 33 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸)) | 
| 35 |  | preq2 4733 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 = 𝑦 → {𝑥, 𝑏} = {𝑥, 𝑦}) | 
| 36 | 35 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = 𝑦 → ({𝑥, 𝑏} ∈ 𝐸 ↔ {𝑥, 𝑦} ∈ 𝐸)) | 
| 37 | 20, 36 | rspc2v 3632 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → {𝑥, 𝑦} ∈ 𝐸)) | 
| 38 | 37 | ad2ant2l 746 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → {𝑥, 𝑦} ∈ 𝐸)) | 
| 39 | 38 | impcom 407 | . . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ∧ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → {𝑥, 𝑦} ∈ 𝐸) | 
| 40 |  | prcom 4731 | . . . . . . . . . . . . . . . . . . . 20
⊢ {𝑦, 𝑎} = {𝑎, 𝑦} | 
| 41 |  | preq2 4733 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 = 𝑦 → {𝑎, 𝑏} = {𝑎, 𝑦}) | 
| 42 | 41 | eleq1d 2825 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 = 𝑦 → ({𝑎, 𝑏} ∈ 𝐸 ↔ {𝑎, 𝑦} ∈ 𝐸)) | 
| 43 | 10, 42 | rspc2v 3632 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → {𝑎, 𝑦} ∈ 𝐸)) | 
| 44 | 43 | ad2ant2rl 749 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (∀𝑧 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → {𝑎, 𝑦} ∈ 𝐸)) | 
| 45 | 44 | impcom 407 | . . . . . . . . . . . . . . . . . . . 20
⊢
((∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ∧ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → {𝑎, 𝑦} ∈ 𝐸) | 
| 46 | 40, 45 | eqeltrid 2844 | . . . . . . . . . . . . . . . . . . 19
⊢
((∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ∧ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → {𝑦, 𝑎} ∈ 𝐸) | 
| 47 | 39, 46 | jca 511 | . . . . . . . . . . . . . . . . . 18
⊢
((∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 ∧ ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵))) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)) | 
| 48 | 47 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢
(∀𝑧 ∈
𝐴 ∀𝑏 ∈ 𝐵 {𝑧, 𝑏} ∈ 𝐸 → (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) | 
| 49 | 8, 48 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ FriendGraph →
(((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) | 
| 50 | 49 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) → (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) | 
| 51 | 50 | impl 455 | . . . . . . . . . . . . . 14
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)) | 
| 52 | 51 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)) | 
| 53 | 2, 34, 52 | 3jca 1128 | . . . . . . . . . . . 12
⊢
(((((𝐺 ∈
FriendGraph ∧ 𝑎 ≠
𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑏 ≠ 𝑦) → ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) | 
| 54 | 53 | ex 412 | . . . . . . . . . . 11
⊢ ((((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑏 ≠ 𝑦 → ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) | 
| 55 | 54 | reximdvva 3206 | . . . . . . . . . 10
⊢ (((𝐺 ∈ FriendGraph ∧ 𝑎 ≠ 𝑥) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) | 
| 56 | 55 | exp31 419 | . . . . . . . . 9
⊢ (𝐺 ∈ FriendGraph →
(𝑎 ≠ 𝑥 → ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))))) | 
| 57 | 56 | com24 95 | . . . . . . . 8
⊢ (𝐺 ∈ FriendGraph →
(∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → ((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑎 ≠ 𝑥 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))))) | 
| 58 | 57 | imp31 417 | . . . . . . 7
⊢ (((𝐺 ∈ FriendGraph ∧
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) ∧ (𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) → (𝑎 ≠ 𝑥 → ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) | 
| 59 | 58 | reximdvva 3206 | . . . . . 6
⊢ ((𝐺 ∈ FriendGraph ∧
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) → (∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) | 
| 60 | 59 | ex 412 | . . . . 5
⊢ (𝐺 ∈ FriendGraph →
(∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → (∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))))) | 
| 61 | 60 | com13 88 | . . . 4
⊢
(∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 → (∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦 → (𝐺 ∈ FriendGraph → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))))) | 
| 62 | 61 | imp 406 | . . 3
⊢
((∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥 ∧ ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) → (𝐺 ∈ FriendGraph → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))) | 
| 63 | 3, 4, 5, 6 | frgrwopreglem1 30332 | . . . 4
⊢ (𝐴 ∈ V ∧ 𝐵 ∈ V) | 
| 64 |  | hashgt12el 14462 | . . . . . 6
⊢ ((𝐴 ∈ V ∧ 1 <
(♯‘𝐴)) →
∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥) | 
| 65 | 64 | ex 412 | . . . . 5
⊢ (𝐴 ∈ V → (1 <
(♯‘𝐴) →
∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 𝑎 ≠ 𝑥)) | 
| 66 |  | hashgt12el 14462 | . . . . . 6
⊢ ((𝐵 ∈ V ∧ 1 <
(♯‘𝐵)) →
∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑏 ≠ 𝑦) | 
| 67 | 66 | ex 412 | . . . . 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 1116 | 1
⊢ ((𝐺 ∈ FriendGraph ∧ 1 <
(♯‘𝐴) ∧ 1
< (♯‘𝐵))
→ ∃𝑎 ∈
𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸))) |