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

Metamath Proof Explorer

Theorem carduniima

Description: The union of the image of a mapping to cardinals is a cardinal. Proposition 11.16 of TakeutiZaring p. 104. (Contributed by NM, 4-Nov-2004)

Ref Expression
Assertion carduniima ( 𝐴 ∈ 𝐵 → ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) → ∪ ( 𝐹 “ 𝐴 ) ∈ ( ω ∪ ran ℵ ) ) )

Proof

Step Hyp Ref Expression
1 ffun ⊢ ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) → Fun 𝐹 )
2 funimaexg ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ 𝐵 ) → ( 𝐹 “ 𝐴 ) ∈ V )
3 1 2 sylan ⊢ ( ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) ∧ 𝐴 ∈ 𝐵 ) → ( 𝐹 “ 𝐴 ) ∈ V )
4 3 expcom ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) → ( 𝐹 “ 𝐴 ) ∈ V ) )
5 fimass ⊢ ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) → ( 𝐹 “ 𝐴 ) ⊆ ( ω ∪ ran ℵ ) )
6 5 sseld ⊢ ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) → ( 𝑥 ∈ ( 𝐹 “ 𝐴 ) → 𝑥 ∈ ( ω ∪ ran ℵ ) ) )
7 iscard3 ⊢ ( ( card ‘ 𝑥 ) = 𝑥 ↔ 𝑥 ∈ ( ω ∪ ran ℵ ) )
8 6 7 imbitrrdi ⊢ ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) → ( 𝑥 ∈ ( 𝐹 “ 𝐴 ) → ( card ‘ 𝑥 ) = 𝑥 ) )
9 8 ralrimiv ⊢ ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) → ∀ 𝑥 ∈ ( 𝐹 “ 𝐴 ) ( card ‘ 𝑥 ) = 𝑥 )
10 carduni ⊢ ( ( 𝐹 “ 𝐴 ) ∈ V → ( ∀ 𝑥 ∈ ( 𝐹 “ 𝐴 ) ( card ‘ 𝑥 ) = 𝑥 → ( card ‘ ∪ ( 𝐹 “ 𝐴 ) ) = ∪ ( 𝐹 “ 𝐴 ) ) )
11 9 10 syl5 ⊢ ( ( 𝐹 “ 𝐴 ) ∈ V → ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) → ( card ‘ ∪ ( 𝐹 “ 𝐴 ) ) = ∪ ( 𝐹 “ 𝐴 ) ) )
12 4 11 syli ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) → ( card ‘ ∪ ( 𝐹 “ 𝐴 ) ) = ∪ ( 𝐹 “ 𝐴 ) ) )
13 iscard3 ⊢ ( ( card ‘ ∪ ( 𝐹 “ 𝐴 ) ) = ∪ ( 𝐹 “ 𝐴 ) ↔ ∪ ( 𝐹 “ 𝐴 ) ∈ ( ω ∪ ran ℵ ) )
14 12 13 imbitrdi ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) → ∪ ( 𝐹 “ 𝐴 ) ∈ ( ω ∪ ran ℵ ) ) )