Step |
Hyp |
Ref |
Expression |
1 |
|
cusgrfi.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
cusgrfi.p |
⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) } |
3 |
|
cusgrfi.f |
⊢ 𝐹 = ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ↦ { 𝑥 , 𝑁 } ) |
4 |
|
diffi |
⊢ ( 𝑉 ∈ Fin → ( 𝑉 ∖ { 𝑁 } ) ∈ Fin ) |
5 |
|
simpr |
⊢ ( ( 𝑁 ∈ 𝑉 ∧ ¬ 𝑉 ∈ Fin ) → ¬ 𝑉 ∈ Fin ) |
6 |
|
snfi |
⊢ { 𝑁 } ∈ Fin |
7 |
|
difinf |
⊢ ( ( ¬ 𝑉 ∈ Fin ∧ { 𝑁 } ∈ Fin ) → ¬ ( 𝑉 ∖ { 𝑁 } ) ∈ Fin ) |
8 |
5 6 7
|
sylancl |
⊢ ( ( 𝑁 ∈ 𝑉 ∧ ¬ 𝑉 ∈ Fin ) → ¬ ( 𝑉 ∖ { 𝑁 } ) ∈ Fin ) |
9 |
8
|
ex |
⊢ ( 𝑁 ∈ 𝑉 → ( ¬ 𝑉 ∈ Fin → ¬ ( 𝑉 ∖ { 𝑁 } ) ∈ Fin ) ) |
10 |
9
|
con4d |
⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑉 ∖ { 𝑁 } ) ∈ Fin → 𝑉 ∈ Fin ) ) |
11 |
4 10
|
impbid2 |
⊢ ( 𝑁 ∈ 𝑉 → ( 𝑉 ∈ Fin ↔ ( 𝑉 ∖ { 𝑁 } ) ∈ Fin ) ) |
12 |
1
|
fvexi |
⊢ 𝑉 ∈ V |
13 |
12
|
difexi |
⊢ ( 𝑉 ∖ { 𝑁 } ) ∈ V |
14 |
|
mptexg |
⊢ ( ( 𝑉 ∖ { 𝑁 } ) ∈ V → ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ↦ { 𝑥 , 𝑁 } ) ∈ V ) |
15 |
13 14
|
mp1i |
⊢ ( 𝑁 ∈ 𝑉 → ( 𝑥 ∈ ( 𝑉 ∖ { 𝑁 } ) ↦ { 𝑥 , 𝑁 } ) ∈ V ) |
16 |
3 15
|
eqeltrid |
⊢ ( 𝑁 ∈ 𝑉 → 𝐹 ∈ V ) |
17 |
1 2 3
|
cusgrfilem2 |
⊢ ( 𝑁 ∈ 𝑉 → 𝐹 : ( 𝑉 ∖ { 𝑁 } ) –1-1-onto→ 𝑃 ) |
18 |
|
f1oeq1 |
⊢ ( 𝑓 = 𝐹 → ( 𝑓 : ( 𝑉 ∖ { 𝑁 } ) –1-1-onto→ 𝑃 ↔ 𝐹 : ( 𝑉 ∖ { 𝑁 } ) –1-1-onto→ 𝑃 ) ) |
19 |
16 17 18
|
spcedv |
⊢ ( 𝑁 ∈ 𝑉 → ∃ 𝑓 𝑓 : ( 𝑉 ∖ { 𝑁 } ) –1-1-onto→ 𝑃 ) |
20 |
|
bren |
⊢ ( ( 𝑉 ∖ { 𝑁 } ) ≈ 𝑃 ↔ ∃ 𝑓 𝑓 : ( 𝑉 ∖ { 𝑁 } ) –1-1-onto→ 𝑃 ) |
21 |
19 20
|
sylibr |
⊢ ( 𝑁 ∈ 𝑉 → ( 𝑉 ∖ { 𝑁 } ) ≈ 𝑃 ) |
22 |
|
enfi |
⊢ ( ( 𝑉 ∖ { 𝑁 } ) ≈ 𝑃 → ( ( 𝑉 ∖ { 𝑁 } ) ∈ Fin ↔ 𝑃 ∈ Fin ) ) |
23 |
21 22
|
syl |
⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑉 ∖ { 𝑁 } ) ∈ Fin ↔ 𝑃 ∈ Fin ) ) |
24 |
11 23
|
bitrd |
⊢ ( 𝑁 ∈ 𝑉 → ( 𝑉 ∈ Fin ↔ 𝑃 ∈ Fin ) ) |