Metamath Proof Explorer

Theorem erdszelem2

Description: Lemma for erdsze . (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypothesis erdszelem1.1 ⊒S=yβˆˆπ’«1…A|Fβ†ΎyIsom<,OyFy∧A∈y
Assertion erdszelem2 ⊒.S∈Fin∧.SβŠ†β„•

Proof

Step Hyp Ref Expression
1 erdszelem1.1 ⊒S=yβˆˆπ’«1…A|Fβ†ΎyIsom<,OyFy∧A∈y
2 fzfi ⊒1…A∈Fin
3 pwfi ⊒1…A∈Fin↔𝒫1…A∈Fin
4 2 3 mpbi βŠ’π’«1…A∈Fin
5 ssrab2 ⊒yβˆˆπ’«1…A|Fβ†ΎyIsom<,OyFy∧A∈yβŠ†π’«1…A
6 1 5 eqsstri ⊒SβŠ†π’«1…A
7 ssfi βŠ’π’«1…A∈Fin∧SβŠ†π’«1…Aβ†’S∈Fin
8 4 6 7 mp2an ⊒S∈Fin
9 hashf ⊒.:VβŸΆβ„•0βˆͺ+∞
10 ffun ⊒.:VβŸΆβ„•0βˆͺ+βˆžβ†’Fun⁑.
11 9 10 ax-mp ⊒Fun⁑.
12 ssv ⊒SβŠ†V
13 9 fdmi ⊒dom⁑.=V
14 12 13 sseqtrri ⊒SβŠ†dom⁑.
15 fores ⊒Fun⁑.∧SβŠ†dom⁑.β†’.β†ΎS:S⟢onto.S
16 11 14 15 mp2an ⊒.β†ΎS:S⟢onto.S
17 fofi ⊒S∈Fin∧.β†ΎS:S⟢onto.Sβ†’.S∈Fin
18 8 16 17 mp2an ⊒.S∈Fin
19 funimass4 ⊒Fun⁑.∧SβŠ†dom⁑.β†’.SβŠ†β„•β†”βˆ€x∈Sxβˆˆβ„•
20 11 14 19 mp2an ⊒.SβŠ†β„•β†”βˆ€x∈Sxβˆˆβ„•
21 1 erdszelem1 ⊒x∈S↔xβŠ†1…A∧Fβ†ΎxIsom<,OxFx∧A∈x
22 ne0i ⊒A∈xβ†’xβ‰ βˆ…
23 22 3ad2ant3 ⊒xβŠ†1…A∧Fβ†ΎxIsom<,OxFx∧A∈xβ†’xβ‰ βˆ…
24 simp1 ⊒xβŠ†1…A∧Fβ†ΎxIsom<,OxFx∧A∈xβ†’xβŠ†1…A
25 ssfi ⊒1…A∈Fin∧xβŠ†1…Aβ†’x∈Fin
26 2 24 25 sylancr ⊒xβŠ†1…A∧Fβ†ΎxIsom<,OxFx∧A∈xβ†’x∈Fin
27 hashnncl ⊒x∈Finβ†’xβˆˆβ„•β†”xβ‰ βˆ…
28 26 27 syl ⊒xβŠ†1…A∧Fβ†ΎxIsom<,OxFx∧A∈xβ†’xβˆˆβ„•β†”xβ‰ βˆ…
29 23 28 mpbird ⊒xβŠ†1…A∧Fβ†ΎxIsom<,OxFx∧A∈xβ†’xβˆˆβ„•
30 21 29 sylbi ⊒x∈Sβ†’xβˆˆβ„•
31 20 30 mprgbir ⊒.SβŠ†β„•
32 18 31 pm3.2i ⊒.S∈Fin∧.SβŠ†β„•