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 ℵ ) ) )