Theorem erdszelem2

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

	Ref	Expression
Hypothesis	erdszelem1.1	⊢ 𝑆 = { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) }
Assertion	erdszelem2	⊢ ( ( ♯ “ 𝑆 ) ∈ Fin ∧ ( ♯ “ 𝑆 ) ⊆ ℕ )

Proof

Step	Hyp	Ref	Expression
1		erdszelem1.1	⊢ 𝑆 = { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) }
2		fzfi	⊢ ( 1 ... 𝐴 ) ∈ Fin
3		pwfi	⊢ ( ( 1 ... 𝐴 ) ∈ Fin ↔ 𝒫 ( 1 ... 𝐴 ) ∈ Fin )
4	2 3	mpbi	⊢ 𝒫 ( 1 ... 𝐴 ) ∈ Fin
5		ssrab2	⊢ { 𝑦 ∈ 𝒫 ( 1 ... 𝐴 ) ∣ ( ( 𝐹 ↾ 𝑦 ) Isom < , 𝑂 ( 𝑦 , ( 𝐹 “ 𝑦 ) ) ∧ 𝐴 ∈ 𝑦 ) } ⊆ 𝒫 ( 1 ... 𝐴 )
6	1 5	eqsstri	⊢ 𝑆 ⊆ 𝒫 ( 1 ... 𝐴 )
7		ssfi	⊢ ( ( 𝒫 ( 1 ... 𝐴 ) ∈ Fin ∧ 𝑆 ⊆ 𝒫 ( 1 ... 𝐴 ) ) → 𝑆 ∈ Fin )
8	4 6 7	mp2an	⊢ 𝑆 ∈ Fin
9		hashf	⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
10		ffun	⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → Fun ♯ )
11	9 10	ax-mp	⊢ Fun ♯
12		ssv	⊢ 𝑆 ⊆ V
13	9	fdmi	⊢ dom ♯ = V
14	12 13	sseqtrri	⊢ 𝑆 ⊆ dom ♯
15		fores	⊢ ( ( Fun ♯ ∧ 𝑆 ⊆ dom ♯ ) → ( ♯ ↾ 𝑆 ) : 𝑆 –onto→ ( ♯ “ 𝑆 ) )
16	11 14 15	mp2an	⊢ ( ♯ ↾ 𝑆 ) : 𝑆 –onto→ ( ♯ “ 𝑆 )
17		fofi	⊢ ( ( 𝑆 ∈ Fin ∧ ( ♯ ↾ 𝑆 ) : 𝑆 –onto→ ( ♯ “ 𝑆 ) ) → ( ♯ “ 𝑆 ) ∈ Fin )
18	8 16 17	mp2an	⊢ ( ♯ “ 𝑆 ) ∈ Fin
19		funimass4	⊢ ( ( Fun ♯ ∧ 𝑆 ⊆ dom ♯ ) → ( ( ♯ “ 𝑆 ) ⊆ ℕ ↔ ∀ 𝑥 ∈ 𝑆 ( ♯ ‘ 𝑥 ) ∈ ℕ ) )
20	11 14 19	mp2an	⊢ ( ( ♯ “ 𝑆 ) ⊆ ℕ ↔ ∀ 𝑥 ∈ 𝑆 ( ♯ ‘ 𝑥 ) ∈ ℕ )
21	1	erdszelem1	⊢ ( 𝑥 ∈ 𝑆 ↔ ( 𝑥 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑥 ) Isom < , 𝑂 ( 𝑥 , ( 𝐹 “ 𝑥 ) ) ∧ 𝐴 ∈ 𝑥 ) )
22		ne0i	⊢ ( 𝐴 ∈ 𝑥 → 𝑥 ≠ ∅ )
23	22	3ad2ant3	⊢ ( ( 𝑥 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑥 ) Isom < , 𝑂 ( 𝑥 , ( 𝐹 “ 𝑥 ) ) ∧ 𝐴 ∈ 𝑥 ) → 𝑥 ≠ ∅ )
24		simp1	⊢ ( ( 𝑥 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑥 ) Isom < , 𝑂 ( 𝑥 , ( 𝐹 “ 𝑥 ) ) ∧ 𝐴 ∈ 𝑥 ) → 𝑥 ⊆ ( 1 ... 𝐴 ) )
25		ssfi	⊢ ( ( ( 1 ... 𝐴 ) ∈ Fin ∧ 𝑥 ⊆ ( 1 ... 𝐴 ) ) → 𝑥 ∈ Fin )
26	2 24 25	sylancr	⊢ ( ( 𝑥 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑥 ) Isom < , 𝑂 ( 𝑥 , ( 𝐹 “ 𝑥 ) ) ∧ 𝐴 ∈ 𝑥 ) → 𝑥 ∈ Fin )
27		hashnncl	⊢ ( 𝑥 ∈ Fin → ( ( ♯ ‘ 𝑥 ) ∈ ℕ ↔ 𝑥 ≠ ∅ ) )
28	26 27	syl	⊢ ( ( 𝑥 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑥 ) Isom < , 𝑂 ( 𝑥 , ( 𝐹 “ 𝑥 ) ) ∧ 𝐴 ∈ 𝑥 ) → ( ( ♯ ‘ 𝑥 ) ∈ ℕ ↔ 𝑥 ≠ ∅ ) )
29	23 28	mpbird	⊢ ( ( 𝑥 ⊆ ( 1 ... 𝐴 ) ∧ ( 𝐹 ↾ 𝑥 ) Isom < , 𝑂 ( 𝑥 , ( 𝐹 “ 𝑥 ) ) ∧ 𝐴 ∈ 𝑥 ) → ( ♯ ‘ 𝑥 ) ∈ ℕ )
30	21 29	sylbi	⊢ ( 𝑥 ∈ 𝑆 → ( ♯ ‘ 𝑥 ) ∈ ℕ )
31	20 30	mprgbir	⊢ ( ♯ “ 𝑆 ) ⊆ ℕ
32	18 31	pm3.2i	⊢ ( ( ♯ “ 𝑆 ) ∈ Fin ∧ ( ♯ “ 𝑆 ) ⊆ ℕ )