This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ⟶ ω