| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . 3
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) | 
| 2 | 1 | isfusgr 29335 | . 2
⊢ (𝐺 ∈ FinUSGraph ↔ (𝐺 ∈ USGraph ∧
(Vtx‘𝐺) ∈
Fin)) | 
| 3 |  | usgrop 29180 | . . . 4
⊢ (𝐺 ∈ USGraph →
〈(Vtx‘𝐺),
(iEdg‘𝐺)〉 ∈
USGraph) | 
| 4 |  | fvex 6919 | . . . . 5
⊢
(iEdg‘𝐺)
∈ V | 
| 5 |  | mptresid 6069 | . . . . . 6
⊢ ( I
↾ {𝑝 ∈
(Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝}) = (𝑞 ∈ {𝑝 ∈ (Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝} ↦ 𝑞) | 
| 6 |  | fvex 6919 | . . . . . . 7
⊢
(Edg‘〈𝑣,
𝑒〉) ∈
V | 
| 7 | 6 | mptrabex 7245 | . . . . . 6
⊢ (𝑞 ∈ {𝑝 ∈ (Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝} ↦ 𝑞) ∈ V | 
| 8 | 5, 7 | eqeltri 2837 | . . . . 5
⊢ ( I
↾ {𝑝 ∈
(Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝}) ∈ V | 
| 9 |  | eleq1 2829 | . . . . . 6
⊢ (𝑒 = (iEdg‘𝐺) → (𝑒 ∈ Fin ↔ (iEdg‘𝐺) ∈ Fin)) | 
| 10 | 9 | adantl 481 | . . . . 5
⊢ ((𝑣 = (Vtx‘𝐺) ∧ 𝑒 = (iEdg‘𝐺)) → (𝑒 ∈ Fin ↔ (iEdg‘𝐺) ∈ Fin)) | 
| 11 |  | eleq1 2829 | . . . . . 6
⊢ (𝑒 = 𝑓 → (𝑒 ∈ Fin ↔ 𝑓 ∈ Fin)) | 
| 12 | 11 | adantl 481 | . . . . 5
⊢ ((𝑣 = 𝑤 ∧ 𝑒 = 𝑓) → (𝑒 ∈ Fin ↔ 𝑓 ∈ Fin)) | 
| 13 |  | vex 3484 | . . . . . . . 8
⊢ 𝑣 ∈ V | 
| 14 |  | vex 3484 | . . . . . . . 8
⊢ 𝑒 ∈ V | 
| 15 | 13, 14 | opvtxfvi 29026 | . . . . . . 7
⊢
(Vtx‘〈𝑣,
𝑒〉) = 𝑣 | 
| 16 | 15 | eqcomi 2746 | . . . . . 6
⊢ 𝑣 = (Vtx‘〈𝑣, 𝑒〉) | 
| 17 |  | eqid 2737 | . . . . . 6
⊢
(Edg‘〈𝑣,
𝑒〉) =
(Edg‘〈𝑣, 𝑒〉) | 
| 18 |  | eqid 2737 | . . . . . 6
⊢ {𝑝 ∈ (Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝} = {𝑝 ∈ (Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝} | 
| 19 |  | eqid 2737 | . . . . . 6
⊢
〈(𝑣 ∖
{𝑛}), ( I ↾ {𝑝 ∈ (Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝})〉 = 〈(𝑣 ∖ {𝑛}), ( I ↾ {𝑝 ∈ (Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝})〉 | 
| 20 | 16, 17, 18, 19 | usgrres1 29332 | . . . . 5
⊢
((〈𝑣, 𝑒〉 ∈ USGraph ∧
𝑛 ∈ 𝑣) → 〈(𝑣 ∖ {𝑛}), ( I ↾ {𝑝 ∈ (Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝})〉 ∈ USGraph) | 
| 21 |  | eleq1 2829 | . . . . . 6
⊢ (𝑓 = ( I ↾ {𝑝 ∈ (Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝}) → (𝑓 ∈ Fin ↔ ( I ↾ {𝑝 ∈ (Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝}) ∈ Fin)) | 
| 22 | 21 | adantl 481 | . . . . 5
⊢ ((𝑤 = (𝑣 ∖ {𝑛}) ∧ 𝑓 = ( I ↾ {𝑝 ∈ (Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝})) → (𝑓 ∈ Fin ↔ ( I ↾ {𝑝 ∈ (Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝}) ∈ Fin)) | 
| 23 | 13, 14 | pm3.2i 470 | . . . . . 6
⊢ (𝑣 ∈ V ∧ 𝑒 ∈ V) | 
| 24 |  | fusgrfisbase 29345 | . . . . . 6
⊢ (((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ 〈𝑣, 𝑒〉 ∈ USGraph ∧
(♯‘𝑣) = 0)
→ 𝑒 ∈
Fin) | 
| 25 | 23, 24 | mp3an1 1450 | . . . . 5
⊢
((〈𝑣, 𝑒〉 ∈ USGraph ∧
(♯‘𝑣) = 0)
→ 𝑒 ∈
Fin) | 
| 26 |  | simpl 482 | . . . . . . . . 9
⊢ (((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ ((𝑦 + 1) ∈ ℕ0
∧ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣))) → (𝑣 ∈ V ∧ 𝑒 ∈ V)) | 
| 27 |  | simprr1 1222 | . . . . . . . . . 10
⊢ (((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ ((𝑦 + 1) ∈ ℕ0
∧ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣))) → 〈𝑣, 𝑒〉 ∈ USGraph) | 
| 28 |  | eleq1 2829 | . . . . . . . . . . . . . 14
⊢
((♯‘𝑣) =
(𝑦 + 1) →
((♯‘𝑣) ∈
ℕ0 ↔ (𝑦 + 1) ∈
ℕ0)) | 
| 29 |  | hashclb 14397 | . . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ V → (𝑣 ∈ Fin ↔
(♯‘𝑣) ∈
ℕ0)) | 
| 30 | 29 | biimprd 248 | . . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ V →
((♯‘𝑣) ∈
ℕ0 → 𝑣 ∈ Fin)) | 
| 31 | 30 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ V ∧ 𝑒 ∈ V) →
((♯‘𝑣) ∈
ℕ0 → 𝑣 ∈ Fin)) | 
| 32 | 31 | com12 32 | . . . . . . . . . . . . . 14
⊢
((♯‘𝑣)
∈ ℕ0 → ((𝑣 ∈ V ∧ 𝑒 ∈ V) → 𝑣 ∈ Fin)) | 
| 33 | 28, 32 | biimtrrdi 254 | . . . . . . . . . . . . 13
⊢
((♯‘𝑣) =
(𝑦 + 1) → ((𝑦 + 1) ∈ ℕ0
→ ((𝑣 ∈ V ∧
𝑒 ∈ V) → 𝑣 ∈ Fin))) | 
| 34 | 33 | 3ad2ant2 1135 | . . . . . . . . . . . 12
⊢
((〈𝑣, 𝑒〉 ∈ USGraph ∧
(♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣) → ((𝑦 + 1) ∈ ℕ0 →
((𝑣 ∈ V ∧ 𝑒 ∈ V) → 𝑣 ∈ Fin))) | 
| 35 | 34 | impcom 407 | . . . . . . . . . . 11
⊢ (((𝑦 + 1) ∈ ℕ0
∧ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) → ((𝑣 ∈ V ∧ 𝑒 ∈ V) → 𝑣 ∈ Fin)) | 
| 36 | 35 | impcom 407 | . . . . . . . . . 10
⊢ (((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ ((𝑦 + 1) ∈ ℕ0
∧ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣))) → 𝑣 ∈ Fin) | 
| 37 |  | opfusgr 29340 | . . . . . . . . . . 11
⊢ ((𝑣 ∈ V ∧ 𝑒 ∈ V) → (〈𝑣, 𝑒〉 ∈ FinUSGraph ↔ (〈𝑣, 𝑒〉 ∈ USGraph ∧ 𝑣 ∈ Fin))) | 
| 38 | 37 | adantr 480 | . . . . . . . . . 10
⊢ (((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ ((𝑦 + 1) ∈ ℕ0
∧ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣))) → (〈𝑣, 𝑒〉 ∈ FinUSGraph ↔ (〈𝑣, 𝑒〉 ∈ USGraph ∧ 𝑣 ∈ Fin))) | 
| 39 | 27, 36, 38 | mpbir2and 713 | . . . . . . . . 9
⊢ (((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ ((𝑦 + 1) ∈ ℕ0
∧ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣))) → 〈𝑣, 𝑒〉 ∈ FinUSGraph) | 
| 40 |  | simprr3 1224 | . . . . . . . . 9
⊢ (((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ ((𝑦 + 1) ∈ ℕ0
∧ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣))) → 𝑛 ∈ 𝑣) | 
| 41 | 26, 39, 40 | 3jca 1129 | . . . . . . . 8
⊢ (((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ ((𝑦 + 1) ∈ ℕ0
∧ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣))) → ((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ 〈𝑣, 𝑒〉 ∈ FinUSGraph ∧ 𝑛 ∈ 𝑣)) | 
| 42 | 23, 41 | mpan 690 | . . . . . . 7
⊢ (((𝑦 + 1) ∈ ℕ0
∧ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) → ((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ 〈𝑣, 𝑒〉 ∈ FinUSGraph ∧ 𝑛 ∈ 𝑣)) | 
| 43 |  | fusgrfisstep 29346 | . . . . . . 7
⊢ (((𝑣 ∈ V ∧ 𝑒 ∈ V) ∧ 〈𝑣, 𝑒〉 ∈ FinUSGraph ∧ 𝑛 ∈ 𝑣) → (( I ↾ {𝑝 ∈ (Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝}) ∈ Fin → 𝑒 ∈ Fin)) | 
| 44 | 42, 43 | syl 17 | . . . . . 6
⊢ (((𝑦 + 1) ∈ ℕ0
∧ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) → (( I ↾ {𝑝 ∈ (Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝}) ∈ Fin → 𝑒 ∈ Fin)) | 
| 45 | 44 | imp 406 | . . . . 5
⊢ ((((𝑦 + 1) ∈ ℕ0
∧ (〈𝑣, 𝑒〉 ∈ USGraph ∧
(♯‘𝑣) = (𝑦 + 1) ∧ 𝑛 ∈ 𝑣)) ∧ ( I ↾ {𝑝 ∈ (Edg‘〈𝑣, 𝑒〉) ∣ 𝑛 ∉ 𝑝}) ∈ Fin) → 𝑒 ∈ Fin) | 
| 46 | 4, 8, 10, 12, 20, 22, 25, 45 | opfi1ind 14551 | . . . 4
⊢
((〈(Vtx‘𝐺), (iEdg‘𝐺)〉 ∈ USGraph ∧
(Vtx‘𝐺) ∈ Fin)
→ (iEdg‘𝐺)
∈ Fin) | 
| 47 | 3, 46 | sylan 580 | . . 3
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) ∈ Fin)
→ (iEdg‘𝐺)
∈ Fin) | 
| 48 |  | eqid 2737 | . . . . 5
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) | 
| 49 |  | eqid 2737 | . . . . 5
⊢
(Edg‘𝐺) =
(Edg‘𝐺) | 
| 50 | 48, 49 | usgredgffibi 29341 | . . . 4
⊢ (𝐺 ∈ USGraph →
((Edg‘𝐺) ∈ Fin
↔ (iEdg‘𝐺)
∈ Fin)) | 
| 51 | 50 | adantr 480 | . . 3
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) ∈ Fin)
→ ((Edg‘𝐺)
∈ Fin ↔ (iEdg‘𝐺) ∈ Fin)) | 
| 52 | 47, 51 | mpbird 257 | . 2
⊢ ((𝐺 ∈ USGraph ∧
(Vtx‘𝐺) ∈ Fin)
→ (Edg‘𝐺) ∈
Fin) | 
| 53 | 2, 52 | sylbi 217 | 1
⊢ (𝐺 ∈ FinUSGraph →
(Edg‘𝐺) ∈
Fin) |