Theorem ackbij1lem10

Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 18-Nov-2014)

	Ref	Expression
Hypothesis	ackbij.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
Assertion	ackbij1lem10	⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω

Proof

Step	Hyp	Ref	Expression
1		ackbij.f	⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) )
2		elinel2	⊢ ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) → 𝑥 ∈ Fin )
3		snfi	⊢ { 𝑦 } ∈ Fin
4		elinel1	⊢ ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) → 𝑥 ∈ 𝒫 ω )
5	4	elpwid	⊢ ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) → 𝑥 ⊆ ω )
6		onfin2	⊢ ω = ( On ∩ Fin )
7		inss2	⊢ ( On ∩ Fin ) ⊆ Fin
8	6 7	eqsstri	⊢ ω ⊆ Fin
9	5 8	sstrdi	⊢ ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) → 𝑥 ⊆ Fin )
10	9	sselda	⊢ ( ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ Fin )
11		pwfi	⊢ ( 𝑦 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin )
12	10 11	sylib	⊢ ( ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → 𝒫 𝑦 ∈ Fin )
13		xpfi	⊢ ( ( { 𝑦 } ∈ Fin ∧ 𝒫 𝑦 ∈ Fin ) → ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin )
14	3 12 13	sylancr	⊢ ( ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝑦 ∈ 𝑥 ) → ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin )
15	14	ralrimiva	⊢ ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) → ∀ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin )
16		iunfi	⊢ ( ( 𝑥 ∈ Fin ∧ ∀ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin ) → ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin )
17	2 15 16	syl2anc	⊢ ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) → ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin )
18		ficardom	⊢ ( ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ∈ Fin → ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) ∈ ω )
19	17 18	syl	⊢ ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) → ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) ∈ ω )
20	1 19	fmpti	⊢ 𝐹 : ( 𝒫 ω ∩ Fin ) ⟶ ω