| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fusgrmaxsize.v | . . . . 5
⊢ 𝑉 = (Vtx‘𝐺) | 
| 2 |  | fusgrmaxsize.e | . . . . 5
⊢ 𝐸 = (Edg‘𝐺) | 
| 3 | 1, 2 | usgredg 29216 | . . . 4
⊢ ((𝐺 ∈ USGraph ∧ 𝑒 ∈ 𝐸) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) | 
| 4 |  | usgrsscusgra.h | . . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐻) | 
| 5 |  | usgrsscusgra.f | . . . . . . . 8
⊢ 𝐹 = (Edg‘𝐻) | 
| 6 | 4, 5 | iscusgredg 29440 | . . . . . . 7
⊢ (𝐻 ∈ ComplUSGraph ↔
(𝐻 ∈ USGraph ∧
∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ 𝐹)) | 
| 7 |  | sneq 4636 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑎 → {𝑘} = {𝑎}) | 
| 8 | 7 | difeq2d 4126 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑎 → (𝑉 ∖ {𝑘}) = (𝑉 ∖ {𝑎})) | 
| 9 |  | preq2 4734 | . . . . . . . . . . . . 13
⊢ (𝑘 = 𝑎 → {𝑛, 𝑘} = {𝑛, 𝑎}) | 
| 10 | 9 | eleq1d 2826 | . . . . . . . . . . . 12
⊢ (𝑘 = 𝑎 → ({𝑛, 𝑘} ∈ 𝐹 ↔ {𝑛, 𝑎} ∈ 𝐹)) | 
| 11 | 8, 10 | raleqbidv 3346 | . . . . . . . . . . 11
⊢ (𝑘 = 𝑎 → (∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ 𝐹 ↔ ∀𝑛 ∈ (𝑉 ∖ {𝑎}){𝑛, 𝑎} ∈ 𝐹)) | 
| 12 | 11 | rspcv 3618 | . . . . . . . . . 10
⊢ (𝑎 ∈ 𝑉 → (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ 𝐹 → ∀𝑛 ∈ (𝑉 ∖ {𝑎}){𝑛, 𝑎} ∈ 𝐹)) | 
| 13 |  | simpl 482 | . . . . . . . . . . . . . . 15
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → 𝑎 ≠ 𝑏) | 
| 14 | 13 | necomd 2996 | . . . . . . . . . . . . . 14
⊢ ((𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → 𝑏 ≠ 𝑎) | 
| 15 | 14 | anim2i 617 | . . . . . . . . . . . . 13
⊢ ((𝑏 ∈ 𝑉 ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → (𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎)) | 
| 16 |  | eldifsn 4786 | . . . . . . . . . . . . 13
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) ↔ (𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎)) | 
| 17 | 15, 16 | sylibr 234 | . . . . . . . . . . . 12
⊢ ((𝑏 ∈ 𝑉 ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → 𝑏 ∈ (𝑉 ∖ {𝑎})) | 
| 18 |  | preq1 4733 | . . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑏 → {𝑛, 𝑎} = {𝑏, 𝑎}) | 
| 19 | 18 | eleq1d 2826 | . . . . . . . . . . . . 13
⊢ (𝑛 = 𝑏 → ({𝑛, 𝑎} ∈ 𝐹 ↔ {𝑏, 𝑎} ∈ 𝐹)) | 
| 20 | 19 | rspcv 3618 | . . . . . . . . . . . 12
⊢ (𝑏 ∈ (𝑉 ∖ {𝑎}) → (∀𝑛 ∈ (𝑉 ∖ {𝑎}){𝑛, 𝑎} ∈ 𝐹 → {𝑏, 𝑎} ∈ 𝐹)) | 
| 21 | 17, 20 | syl 17 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ 𝑉 ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → (∀𝑛 ∈ (𝑉 ∖ {𝑎}){𝑛, 𝑎} ∈ 𝐹 → {𝑏, 𝑎} ∈ 𝐹)) | 
| 22 |  | prcom 4732 | . . . . . . . . . . . . . . . 16
⊢ {𝑎, 𝑏} = {𝑏, 𝑎} | 
| 23 | 22 | eqeq2i 2750 | . . . . . . . . . . . . . . 15
⊢ (𝑒 = {𝑎, 𝑏} ↔ 𝑒 = {𝑏, 𝑎}) | 
| 24 |  | eqcom 2744 | . . . . . . . . . . . . . . 15
⊢ (𝑒 = {𝑏, 𝑎} ↔ {𝑏, 𝑎} = 𝑒) | 
| 25 | 23, 24 | sylbb 219 | . . . . . . . . . . . . . 14
⊢ (𝑒 = {𝑎, 𝑏} → {𝑏, 𝑎} = 𝑒) | 
| 26 | 25 | eleq1d 2826 | . . . . . . . . . . . . 13
⊢ (𝑒 = {𝑎, 𝑏} → ({𝑏, 𝑎} ∈ 𝐹 ↔ 𝑒 ∈ 𝐹)) | 
| 27 | 26 | biimpd 229 | . . . . . . . . . . . 12
⊢ (𝑒 = {𝑎, 𝑏} → ({𝑏, 𝑎} ∈ 𝐹 → 𝑒 ∈ 𝐹)) | 
| 28 | 27 | ad2antll 729 | . . . . . . . . . . 11
⊢ ((𝑏 ∈ 𝑉 ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → ({𝑏, 𝑎} ∈ 𝐹 → 𝑒 ∈ 𝐹)) | 
| 29 | 21, 28 | syld 47 | . . . . . . . . . 10
⊢ ((𝑏 ∈ 𝑉 ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → (∀𝑛 ∈ (𝑉 ∖ {𝑎}){𝑛, 𝑎} ∈ 𝐹 → 𝑒 ∈ 𝐹)) | 
| 30 | 12, 29 | syl9 77 | . . . . . . . . 9
⊢ (𝑎 ∈ 𝑉 → ((𝑏 ∈ 𝑉 ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ 𝐹 → 𝑒 ∈ 𝐹))) | 
| 31 | 30 | impl 455 | . . . . . . . 8
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → (∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ 𝐹 → 𝑒 ∈ 𝐹)) | 
| 32 | 31 | adantld 490 | . . . . . . 7
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → ((𝐻 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘}){𝑛, 𝑘} ∈ 𝐹) → 𝑒 ∈ 𝐹)) | 
| 33 | 6, 32 | biimtrid 242 | . . . . . 6
⊢ (((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏})) → (𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹)) | 
| 34 | 33 | ex 412 | . . . . 5
⊢ ((𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) → ((𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → (𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹))) | 
| 35 | 34 | rexlimivv 3201 | . . . 4
⊢
(∃𝑎 ∈
𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑒 = {𝑎, 𝑏}) → (𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹)) | 
| 36 | 3, 35 | syl 17 | . . 3
⊢ ((𝐺 ∈ USGraph ∧ 𝑒 ∈ 𝐸) → (𝐻 ∈ ComplUSGraph → 𝑒 ∈ 𝐹)) | 
| 37 | 36 | impancom 451 | . 2
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) →
(𝑒 ∈ 𝐸 → 𝑒 ∈ 𝐹)) | 
| 38 | 37 | ssrdv 3989 | 1
⊢ ((𝐺 ∈ USGraph ∧ 𝐻 ∈ ComplUSGraph) →
𝐸 ⊆ 𝐹) |