Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
2 |
1
|
isfusgr |
⊢ ( 𝐺 ∈ FinUSGraph ↔ ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) ∈ Fin ) ) |
3 |
|
usgrop |
⊢ ( 𝐺 ∈ USGraph → 〈 ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) 〉 ∈ USGraph ) |
4 |
|
fvex |
⊢ ( iEdg ‘ 𝐺 ) ∈ V |
5 |
|
mptresid |
⊢ ( I ↾ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } ) = ( 𝑞 ∈ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } ↦ 𝑞 ) |
6 |
|
fvex |
⊢ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∈ V |
7 |
6
|
mptrabex |
⊢ ( 𝑞 ∈ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } ↦ 𝑞 ) ∈ V |
8 |
5 7
|
eqeltri |
⊢ ( I ↾ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } ) ∈ V |
9 |
|
eleq1 |
⊢ ( 𝑒 = ( iEdg ‘ 𝐺 ) → ( 𝑒 ∈ Fin ↔ ( iEdg ‘ 𝐺 ) ∈ Fin ) ) |
10 |
9
|
adantl |
⊢ ( ( 𝑣 = ( Vtx ‘ 𝐺 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) → ( 𝑒 ∈ Fin ↔ ( iEdg ‘ 𝐺 ) ∈ Fin ) ) |
11 |
|
eleq1 |
⊢ ( 𝑒 = 𝑓 → ( 𝑒 ∈ Fin ↔ 𝑓 ∈ Fin ) ) |
12 |
11
|
adantl |
⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝑒 ∈ Fin ↔ 𝑓 ∈ Fin ) ) |
13 |
|
vex |
⊢ 𝑣 ∈ V |
14 |
|
vex |
⊢ 𝑒 ∈ V |
15 |
13 14
|
opvtxfvi |
⊢ ( Vtx ‘ 〈 𝑣 , 𝑒 〉 ) = 𝑣 |
16 |
15
|
eqcomi |
⊢ 𝑣 = ( Vtx ‘ 〈 𝑣 , 𝑒 〉 ) |
17 |
|
eqid |
⊢ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) = ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) |
18 |
|
eqid |
⊢ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } = { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } |
19 |
|
eqid |
⊢ 〈 ( 𝑣 ∖ { 𝑛 } ) , ( I ↾ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } ) 〉 = 〈 ( 𝑣 ∖ { 𝑛 } ) , ( I ↾ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } ) 〉 |
20 |
16 17 18 19
|
usgrres1 |
⊢ ( ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ 𝑛 ∈ 𝑣 ) → 〈 ( 𝑣 ∖ { 𝑛 } ) , ( I ↾ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } ) 〉 ∈ USGraph ) |
21 |
|
eleq1 |
⊢ ( 𝑓 = ( I ↾ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } ) → ( 𝑓 ∈ Fin ↔ ( I ↾ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } ) ∈ Fin ) ) |
22 |
21
|
adantl |
⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = ( I ↾ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } ) ) → ( 𝑓 ∈ Fin ↔ ( I ↾ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } ) ∈ Fin ) ) |
23 |
13 14
|
pm3.2i |
⊢ ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) |
24 |
|
fusgrfisbase |
⊢ ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = 0 ) → 𝑒 ∈ Fin ) |
25 |
23 24
|
mp3an1 |
⊢ ( ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = 0 ) → 𝑒 ∈ Fin ) |
26 |
|
simpl |
⊢ ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ) → ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ) |
27 |
|
simprr1 |
⊢ ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ) → 〈 𝑣 , 𝑒 〉 ∈ USGraph ) |
28 |
|
eleq1 |
⊢ ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( ( ♯ ‘ 𝑣 ) ∈ ℕ0 ↔ ( 𝑦 + 1 ) ∈ ℕ0 ) ) |
29 |
|
hashclb |
⊢ ( 𝑣 ∈ V → ( 𝑣 ∈ Fin ↔ ( ♯ ‘ 𝑣 ) ∈ ℕ0 ) ) |
30 |
29
|
biimprd |
⊢ ( 𝑣 ∈ V → ( ( ♯ ‘ 𝑣 ) ∈ ℕ0 → 𝑣 ∈ Fin ) ) |
31 |
30
|
adantr |
⊢ ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) → ( ( ♯ ‘ 𝑣 ) ∈ ℕ0 → 𝑣 ∈ Fin ) ) |
32 |
31
|
com12 |
⊢ ( ( ♯ ‘ 𝑣 ) ∈ ℕ0 → ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) → 𝑣 ∈ Fin ) ) |
33 |
28 32
|
syl6bir |
⊢ ( ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) → ( ( 𝑦 + 1 ) ∈ ℕ0 → ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) → 𝑣 ∈ Fin ) ) ) |
34 |
33
|
3ad2ant2 |
⊢ ( ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) → ( ( 𝑦 + 1 ) ∈ ℕ0 → ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) → 𝑣 ∈ Fin ) ) ) |
35 |
34
|
impcom |
⊢ ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) → ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) → 𝑣 ∈ Fin ) ) |
36 |
35
|
impcom |
⊢ ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ) → 𝑣 ∈ Fin ) |
37 |
|
opfusgr |
⊢ ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) → ( 〈 𝑣 , 𝑒 〉 ∈ FinUSGraph ↔ ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ 𝑣 ∈ Fin ) ) ) |
38 |
37
|
adantr |
⊢ ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ) → ( 〈 𝑣 , 𝑒 〉 ∈ FinUSGraph ↔ ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ 𝑣 ∈ Fin ) ) ) |
39 |
27 36 38
|
mpbir2and |
⊢ ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ) → 〈 𝑣 , 𝑒 〉 ∈ FinUSGraph ) |
40 |
|
simprr3 |
⊢ ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ) → 𝑛 ∈ 𝑣 ) |
41 |
26 39 40
|
3jca |
⊢ ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ) → ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ 〈 𝑣 , 𝑒 〉 ∈ FinUSGraph ∧ 𝑛 ∈ 𝑣 ) ) |
42 |
23 41
|
mpan |
⊢ ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) → ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ 〈 𝑣 , 𝑒 〉 ∈ FinUSGraph ∧ 𝑛 ∈ 𝑣 ) ) |
43 |
|
fusgrfisstep |
⊢ ( ( ( 𝑣 ∈ V ∧ 𝑒 ∈ V ) ∧ 〈 𝑣 , 𝑒 〉 ∈ FinUSGraph ∧ 𝑛 ∈ 𝑣 ) → ( ( I ↾ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } ) ∈ Fin → 𝑒 ∈ Fin ) ) |
44 |
42 43
|
syl |
⊢ ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) → ( ( I ↾ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } ) ∈ Fin → 𝑒 ∈ Fin ) ) |
45 |
44
|
imp |
⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 〈 𝑣 , 𝑒 〉 ∈ USGraph ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ ( I ↾ { 𝑝 ∈ ( Edg ‘ 〈 𝑣 , 𝑒 〉 ) ∣ 𝑛 ∉ 𝑝 } ) ∈ Fin ) → 𝑒 ∈ Fin ) |
46 |
4 8 10 12 20 22 25 45
|
opfi1ind |
⊢ ( ( 〈 ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) 〉 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) ∈ Fin ) → ( iEdg ‘ 𝐺 ) ∈ Fin ) |
47 |
3 46
|
sylan |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) ∈ Fin ) → ( iEdg ‘ 𝐺 ) ∈ Fin ) |
48 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
49 |
|
eqid |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) |
50 |
48 49
|
usgredgffibi |
⊢ ( 𝐺 ∈ USGraph → ( ( Edg ‘ 𝐺 ) ∈ Fin ↔ ( iEdg ‘ 𝐺 ) ∈ Fin ) ) |
51 |
50
|
adantr |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) ∈ Fin ) → ( ( Edg ‘ 𝐺 ) ∈ Fin ↔ ( iEdg ‘ 𝐺 ) ∈ Fin ) ) |
52 |
47 51
|
mpbird |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( Vtx ‘ 𝐺 ) ∈ Fin ) → ( Edg ‘ 𝐺 ) ∈ Fin ) |
53 |
2 52
|
sylbi |
⊢ ( 𝐺 ∈ FinUSGraph → ( Edg ‘ 𝐺 ) ∈ Fin ) |