Proof of Theorem usgrislfuspgr
Step | Hyp | Ref
| Expression |
1 | | usgruspgr 27558 |
. . 3
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
USPGraph) |
2 | | usgrislfuspgr.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
3 | | usgrislfuspgr.i |
. . . . 5
⊢ 𝐼 = (iEdg‘𝐺) |
4 | 2, 3 | usgrfs 27537 |
. . . 4
⊢ (𝐺 ∈ USGraph → 𝐼:dom 𝐼–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
5 | | f1f 6662 |
. . . . 5
⊢ (𝐼:dom 𝐼–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} → 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}) |
6 | | 2re 12057 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
7 | 6 | leidi 11519 |
. . . . . . . . . 10
⊢ 2 ≤
2 |
8 | 7 | a1i 11 |
. . . . . . . . 9
⊢
((♯‘𝑥) =
2 → 2 ≤ 2) |
9 | | breq2 5077 |
. . . . . . . . 9
⊢
((♯‘𝑥) =
2 → (2 ≤ (♯‘𝑥) ↔ 2 ≤ 2)) |
10 | 8, 9 | mpbird 256 |
. . . . . . . 8
⊢
((♯‘𝑥) =
2 → 2 ≤ (♯‘𝑥)) |
11 | 10 | a1i 11 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝑉 → ((♯‘𝑥) = 2 → 2 ≤
(♯‘𝑥))) |
12 | 11 | ss2rabi 4009 |
. . . . . 6
⊢ {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤
(♯‘𝑥)} |
13 | 12 | a1i 11 |
. . . . 5
⊢ (𝐼:dom 𝐼–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} → {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⊆ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) |
14 | 5, 13 | fssd 6610 |
. . . 4
⊢ (𝐼:dom 𝐼–1-1→{𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} → 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) |
15 | 4, 14 | syl 17 |
. . 3
⊢ (𝐺 ∈ USGraph → 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) |
16 | 1, 15 | jca 512 |
. 2
⊢ (𝐺 ∈ USGraph → (𝐺 ∈ USPGraph ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})) |
17 | 2, 3 | uspgrf 27534 |
. . . 4
⊢ (𝐺 ∈ USPGraph → 𝐼:dom 𝐼–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
18 | | df-f1 6431 |
. . . . . 6
⊢ (𝐼:dom 𝐼–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
↔ (𝐼:dom 𝐼⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∧ Fun ◡𝐼)) |
19 | | fin 6646 |
. . . . . . . . . . 11
⊢ (𝐼:dom 𝐼⟶({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∩ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(♯‘𝑥)}) ↔
(𝐼:dom 𝐼⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})) |
20 | | umgrislfupgrlem 27502 |
. . . . . . . . . . . 12
⊢ ({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∩ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(♯‘𝑥)}) =
{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) =
2} |
21 | | feq3 6575 |
. . . . . . . . . . . 12
⊢ (({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∩ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(♯‘𝑥)}) =
{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) = 2}
→ (𝐼:dom 𝐼⟶({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∩ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(♯‘𝑥)}) ↔
𝐼:dom 𝐼⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) =
2})) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐼:dom 𝐼⟶({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∩ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(♯‘𝑥)}) ↔
𝐼:dom 𝐼⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) =
2}) |
23 | 19, 22 | sylbb1 236 |
. . . . . . . . . 10
⊢ ((𝐼:dom 𝐼⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) → 𝐼:dom 𝐼⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) =
2}) |
24 | 23 | anim1i 615 |
. . . . . . . . 9
⊢ (((𝐼:dom 𝐼⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) ∧ Fun ◡𝐼) → (𝐼:dom 𝐼⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) = 2}
∧ Fun ◡𝐼)) |
25 | | df-f1 6431 |
. . . . . . . . 9
⊢ (𝐼:dom 𝐼–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) = 2}
↔ (𝐼:dom 𝐼⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) = 2}
∧ Fun ◡𝐼)) |
26 | 24, 25 | sylibr 233 |
. . . . . . . 8
⊢ (((𝐼:dom 𝐼⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) ∧ Fun ◡𝐼) → 𝐼:dom 𝐼–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) =
2}) |
27 | 26 | ex 413 |
. . . . . . 7
⊢ ((𝐼:dom 𝐼⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) → (Fun ◡𝐼 → 𝐼:dom 𝐼–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) =
2})) |
28 | 27 | impancom 452 |
. . . . . 6
⊢ ((𝐼:dom 𝐼⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∧ Fun ◡𝐼) → (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} → 𝐼:dom 𝐼–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) =
2})) |
29 | 18, 28 | sylbi 216 |
. . . . 5
⊢ (𝐼:dom 𝐼–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
→ (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)} → 𝐼:dom 𝐼–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) =
2})) |
30 | 29 | imp 407 |
. . . 4
⊢ ((𝐼:dom 𝐼–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) → 𝐼:dom 𝐼–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) =
2}) |
31 | 17, 30 | sylan 580 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) → 𝐼:dom 𝐼–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) =
2}) |
32 | 2, 3 | isusgr 27533 |
. . . 4
⊢ (𝐺 ∈ USPGraph → (𝐺 ∈ USGraph ↔ 𝐼:dom 𝐼–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) =
2})) |
33 | 32 | adantr 481 |
. . 3
⊢ ((𝐺 ∈ USPGraph ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) → (𝐺 ∈ USGraph ↔ 𝐼:dom 𝐼–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) =
2})) |
34 | 31, 33 | mpbird 256 |
. 2
⊢ ((𝐺 ∈ USPGraph ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)}) → 𝐺 ∈ USGraph) |
35 | 16, 34 | impbii 208 |
1
⊢ (𝐺 ∈ USGraph ↔ (𝐺 ∈ USPGraph ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (♯‘𝑥)})) |