| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp2 1138 | . . 3
⊢ ((𝐺 ∈ ComplGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → 𝐴 ∈ 𝑉) | 
| 2 |  | simp3 1139 | . . 3
⊢ ((𝐺 ∈ ComplGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → 𝐵 ∈ (𝑉 ∖ {𝐴})) | 
| 3 |  | eleq1 2829 | . . . . . . 7
⊢ (𝑎 = 𝐴 → (𝑎 ∈ 𝑉 ↔ 𝐴 ∈ 𝑉)) | 
| 4 |  | sneq 4636 | . . . . . . . . 9
⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴}) | 
| 5 | 4 | difeq2d 4126 | . . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑉 ∖ {𝑎}) = (𝑉 ∖ {𝐴})) | 
| 6 | 5 | eleq2d 2827 | . . . . . . 7
⊢ (𝑎 = 𝐴 → (𝑏 ∈ (𝑉 ∖ {𝑎}) ↔ 𝑏 ∈ (𝑉 ∖ {𝐴}))) | 
| 7 | 3, 6 | anbi12d 632 | . . . . . 6
⊢ (𝑎 = 𝐴 → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) ↔ (𝐴 ∈ 𝑉 ∧ 𝑏 ∈ (𝑉 ∖ {𝐴})))) | 
| 8 |  | preq1 4733 | . . . . . . . 8
⊢ (𝑎 = 𝐴 → {𝑎, 𝑏} = {𝐴, 𝑏}) | 
| 9 | 8 | sseq1d 4015 | . . . . . . 7
⊢ (𝑎 = 𝐴 → ({𝑎, 𝑏} ⊆ 𝑒 ↔ {𝐴, 𝑏} ⊆ 𝑒)) | 
| 10 | 9 | rexbidv 3179 | . . . . . 6
⊢ (𝑎 = 𝐴 → (∃𝑒 ∈ 𝐸 {𝑎, 𝑏} ⊆ 𝑒 ↔ ∃𝑒 ∈ 𝐸 {𝐴, 𝑏} ⊆ 𝑒)) | 
| 11 | 7, 10 | imbi12d 344 | . . . . 5
⊢ (𝑎 = 𝐴 → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → ∃𝑒 ∈ 𝐸 {𝑎, 𝑏} ⊆ 𝑒) ↔ ((𝐴 ∈ 𝑉 ∧ 𝑏 ∈ (𝑉 ∖ {𝐴})) → ∃𝑒 ∈ 𝐸 {𝐴, 𝑏} ⊆ 𝑒))) | 
| 12 |  | eleq1 2829 | . . . . . . 7
⊢ (𝑏 = 𝐵 → (𝑏 ∈ (𝑉 ∖ {𝐴}) ↔ 𝐵 ∈ (𝑉 ∖ {𝐴}))) | 
| 13 | 12 | anbi2d 630 | . . . . . 6
⊢ (𝑏 = 𝐵 → ((𝐴 ∈ 𝑉 ∧ 𝑏 ∈ (𝑉 ∖ {𝐴})) ↔ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})))) | 
| 14 |  | preq2 4734 | . . . . . . . 8
⊢ (𝑏 = 𝐵 → {𝐴, 𝑏} = {𝐴, 𝐵}) | 
| 15 | 14 | sseq1d 4015 | . . . . . . 7
⊢ (𝑏 = 𝐵 → ({𝐴, 𝑏} ⊆ 𝑒 ↔ {𝐴, 𝐵} ⊆ 𝑒)) | 
| 16 | 15 | rexbidv 3179 | . . . . . 6
⊢ (𝑏 = 𝐵 → (∃𝑒 ∈ 𝐸 {𝐴, 𝑏} ⊆ 𝑒 ↔ ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒)) | 
| 17 | 13, 16 | imbi12d 344 | . . . . 5
⊢ (𝑏 = 𝐵 → (((𝐴 ∈ 𝑉 ∧ 𝑏 ∈ (𝑉 ∖ {𝐴})) → ∃𝑒 ∈ 𝐸 {𝐴, 𝑏} ⊆ 𝑒) ↔ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒))) | 
| 18 | 11, 17 | sylan9bb 509 | . . . 4
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → ∃𝑒 ∈ 𝐸 {𝑎, 𝑏} ⊆ 𝑒) ↔ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒))) | 
| 19 |  | cplgredgex.1 | . . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) | 
| 20 |  | cplgredgex.2 | . . . . . . . 8
⊢ 𝐸 = (Edg‘𝐺) | 
| 21 | 19, 20 | iscplgredg 29434 | . . . . . . 7
⊢ (𝐺 ∈ ComplGraph → (𝐺 ∈ ComplGraph ↔
∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑒 ∈ 𝐸 {𝑎, 𝑏} ⊆ 𝑒)) | 
| 22 | 21 | ibi 267 | . . . . . 6
⊢ (𝐺 ∈ ComplGraph →
∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑒 ∈ 𝐸 {𝑎, 𝑏} ⊆ 𝑒) | 
| 23 |  | rsp2 3277 | . . . . . 6
⊢
(∀𝑎 ∈
𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑒 ∈ 𝐸 {𝑎, 𝑏} ⊆ 𝑒 → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → ∃𝑒 ∈ 𝐸 {𝑎, 𝑏} ⊆ 𝑒)) | 
| 24 | 22, 23 | syl 17 | . . . . 5
⊢ (𝐺 ∈ ComplGraph →
((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → ∃𝑒 ∈ 𝐸 {𝑎, 𝑏} ⊆ 𝑒)) | 
| 25 | 24 | 3ad2ant1 1134 | . . . 4
⊢ ((𝐺 ∈ ComplGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ (𝑉 ∖ {𝑎})) → ∃𝑒 ∈ 𝐸 {𝑎, 𝑏} ⊆ 𝑒)) | 
| 26 | 1, 2, 18, 25 | vtocl2d 3562 | . . 3
⊢ ((𝐺 ∈ ComplGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒)) | 
| 27 | 1, 2, 26 | mp2and 699 | . 2
⊢ ((𝐺 ∈ ComplGraph ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒) | 
| 28 | 27 | 3expib 1123 | 1
⊢ (𝐺 ∈ ComplGraph →
((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ (𝑉 ∖ {𝐴})) → ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒)) |