Step | Hyp | Ref
| Expression |
1 | | nfielex 8074 |
. . . . 5
⊢ (¬
𝑉 ∈ Fin →
∃𝑛 𝑛 ∈ 𝑉) |
2 | | cusisusgra 25987 |
. . . . . . . 8
⊢ (𝑉 ComplUSGrph 𝐸 → 𝑉 USGrph 𝐸) |
3 | | usgrav 25867 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝑉 ComplUSGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
5 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = 𝑝 → (𝑒 = {𝑣, 𝑛} ↔ 𝑝 = {𝑣, 𝑛})) |
6 | 5 | anbi2d 736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = 𝑝 → ((𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛}) ↔ (𝑣 ≠ 𝑛 ∧ 𝑝 = {𝑣, 𝑛}))) |
7 | 6 | rexbidv 3034 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = 𝑝 → (∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛}) ↔ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑝 = {𝑣, 𝑛}))) |
8 | 7 | cbvrabv 3172 |
. . . . . . . . . . . . . . 15
⊢ {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} = {𝑝 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑝 = {𝑣, 𝑛})} |
9 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ (𝑉 ∖ {𝑛}) ↦ {𝑝, 𝑛}) = (𝑝 ∈ (𝑉 ∖ {𝑛}) ↦ {𝑝, 𝑛}) |
10 | 8, 9 | cusgrafilem3 26009 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ V ∧ 𝑛 ∈ 𝑉) → (¬ 𝑉 ∈ Fin → ¬ {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ∈ Fin)) |
11 | 10 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ V → (𝑛 ∈ 𝑉 → (¬ 𝑉 ∈ Fin → ¬ {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ∈ Fin))) |
12 | 11 | com13 86 |
. . . . . . . . . . . 12
⊢ (¬
𝑉 ∈ Fin → (𝑛 ∈ 𝑉 → (𝑉 ∈ V → ¬ {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ∈ Fin))) |
13 | 12 | imp 444 |
. . . . . . . . . . 11
⊢ ((¬
𝑉 ∈ Fin ∧ 𝑛 ∈ 𝑉) → (𝑉 ∈ V → ¬ {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ∈ Fin)) |
14 | 13 | com12 32 |
. . . . . . . . . 10
⊢ (𝑉 ∈ V → ((¬ 𝑉 ∈ Fin ∧ 𝑛 ∈ 𝑉) → ¬ {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ∈ Fin)) |
15 | 8 | cusgrafilem1 26007 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑛 ∈ 𝑉) → {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ⊆ ran 𝐸) |
16 | | ssfi 8065 |
. . . . . . . . . . . . . . . . 17
⊢ ((ran
𝐸 ∈ Fin ∧ {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ⊆ ran 𝐸) → {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ∈ Fin) |
17 | 16 | expcom 450 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ⊆ ran 𝐸 → (ran 𝐸 ∈ Fin → {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ∈ Fin)) |
18 | 17 | con3d 147 |
. . . . . . . . . . . . . . 15
⊢ ({𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ⊆ ran 𝐸 → (¬ {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ∈ Fin → ¬ ran 𝐸 ∈ Fin)) |
19 | | rnfi 8132 |
. . . . . . . . . . . . . . . 16
⊢ (𝐸 ∈ Fin → ran 𝐸 ∈ Fin) |
20 | 19 | con3i 149 |
. . . . . . . . . . . . . . 15
⊢ (¬
ran 𝐸 ∈ Fin →
¬ 𝐸 ∈
Fin) |
21 | 18, 20 | syl6 34 |
. . . . . . . . . . . . . 14
⊢ ({𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ⊆ ran 𝐸 → (¬ {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ∈ Fin → ¬ 𝐸 ∈ Fin)) |
22 | 15, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝑛 ∈ 𝑉) → (¬ {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ∈ Fin → ¬ 𝐸 ∈ Fin)) |
23 | 22 | expcom 450 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑉 → (𝑉 ComplUSGrph 𝐸 → (¬ {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ∈ Fin → ¬ 𝐸 ∈ Fin))) |
24 | 23 | com23 84 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ 𝑉 → (¬ {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ∈ Fin → (𝑉 ComplUSGrph 𝐸 → ¬ 𝐸 ∈ Fin))) |
25 | 24 | adantl 481 |
. . . . . . . . . 10
⊢ ((¬
𝑉 ∈ Fin ∧ 𝑛 ∈ 𝑉) → (¬ {𝑒 ∈ 𝒫 𝑉 ∣ ∃𝑣 ∈ 𝑉 (𝑣 ≠ 𝑛 ∧ 𝑒 = {𝑣, 𝑛})} ∈ Fin → (𝑉 ComplUSGrph 𝐸 → ¬ 𝐸 ∈ Fin))) |
26 | 14, 25 | sylcom 30 |
. . . . . . . . 9
⊢ (𝑉 ∈ V → ((¬ 𝑉 ∈ Fin ∧ 𝑛 ∈ 𝑉) → (𝑉 ComplUSGrph 𝐸 → ¬ 𝐸 ∈ Fin))) |
27 | 26 | com23 84 |
. . . . . . . 8
⊢ (𝑉 ∈ V → (𝑉 ComplUSGrph 𝐸 → ((¬ 𝑉 ∈ Fin ∧ 𝑛 ∈ 𝑉) → ¬ 𝐸 ∈ Fin))) |
28 | 27 | adantr 480 |
. . . . . . 7
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ComplUSGrph 𝐸 → ((¬ 𝑉 ∈ Fin ∧ 𝑛 ∈ 𝑉) → ¬ 𝐸 ∈ Fin))) |
29 | 4, 28 | mpcom 37 |
. . . . . 6
⊢ (𝑉 ComplUSGrph 𝐸 → ((¬ 𝑉 ∈ Fin ∧ 𝑛 ∈ 𝑉) → ¬ 𝐸 ∈ Fin)) |
30 | 29 | com12 32 |
. . . . 5
⊢ ((¬
𝑉 ∈ Fin ∧ 𝑛 ∈ 𝑉) → (𝑉 ComplUSGrph 𝐸 → ¬ 𝐸 ∈ Fin)) |
31 | 1, 30 | exlimddv 1850 |
. . . 4
⊢ (¬
𝑉 ∈ Fin → (𝑉 ComplUSGrph 𝐸 → ¬ 𝐸 ∈ Fin)) |
32 | 31 | com12 32 |
. . 3
⊢ (𝑉 ComplUSGrph 𝐸 → (¬ 𝑉 ∈ Fin → ¬ 𝐸 ∈ Fin)) |
33 | 32 | con4d 113 |
. 2
⊢ (𝑉 ComplUSGrph 𝐸 → (𝐸 ∈ Fin → 𝑉 ∈ Fin)) |
34 | 33 | imp 444 |
1
⊢ ((𝑉 ComplUSGrph 𝐸 ∧ 𝐸 ∈ Fin) → 𝑉 ∈ Fin) |