Metamath Proof Explorer

Theorem cardinfima

Description: If a mapping to cardinals has an infinite value, then the union of its image is an infinite cardinal. Corollary 11.17 of TakeutiZaring p. 104. (Contributed by NM, 4-Nov-2004)

Ref Expression
Assertion cardinfima ( 𝐴 ∈ 𝐵 → ( ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) ∧ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ ) → ∪ ( 𝐹 “ 𝐴 ) ∈ ran ℵ ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ V )
2 isinfcard ⊢ ( ( ω ⊆ ( 𝐹 ‘ 𝑥 ) ∧ ( card ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ )
3 2 bicomi ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ ↔ ( ω ⊆ ( 𝐹 ‘ 𝑥 ) ∧ ( card ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) ) )
4 3 simplbi ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ → ω ⊆ ( 𝐹 ‘ 𝑥 ) )
5 ffn ⊢ ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) → 𝐹 Fn 𝐴 )
6 fnfvelrn ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 )
7 6 ex ⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 ) )
8 fnima ⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 “ 𝐴 ) = ran 𝐹 )
9 8 eleq2d ⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝐴 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ran 𝐹 ) )
10 7 9 sylibrd ⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝐴 ) ) )
11 elssuni ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 “ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ∪ ( 𝐹 “ 𝐴 ) )
12 10 11 syl6 ⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ 𝐴 → ( 𝐹 ‘ 𝑥 ) ⊆ ∪ ( 𝐹 “ 𝐴 ) ) )
13 12 imp ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ∪ ( 𝐹 “ 𝐴 ) )
14 5 13 sylan ⊢ ( ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ⊆ ∪ ( 𝐹 “ 𝐴 ) )
15 4 14 sylan9ssr ⊢ ( ( ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ ) → ω ⊆ ∪ ( 𝐹 “ 𝐴 ) )
16 15 anasss ⊢ ( ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ ) ) → ω ⊆ ∪ ( 𝐹 “ 𝐴 ) )
17 16 a1i ⊢ ( 𝐴 ∈ V → ( ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ ) ) → ω ⊆ ∪ ( 𝐹 “ 𝐴 ) ) )
18 carduniima ⊢ ( 𝐴 ∈ V → ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) → ∪ ( 𝐹 “ 𝐴 ) ∈ ( ω ∪ ran ℵ ) ) )
19 iscard3 ⊢ ( ( card ‘ ∪ ( 𝐹 “ 𝐴 ) ) = ∪ ( 𝐹 “ 𝐴 ) ↔ ∪ ( 𝐹 “ 𝐴 ) ∈ ( ω ∪ ran ℵ ) )
20 18 19 syl6ibr ⊢ ( 𝐴 ∈ V → ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) → ( card ‘ ∪ ( 𝐹 “ 𝐴 ) ) = ∪ ( 𝐹 “ 𝐴 ) ) )
21 20 adantrd ⊢ ( 𝐴 ∈ V → ( ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ ) ) → ( card ‘ ∪ ( 𝐹 “ 𝐴 ) ) = ∪ ( 𝐹 “ 𝐴 ) ) )
22 17 21 jcad ⊢ ( 𝐴 ∈ V → ( ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ ) ) → ( ω ⊆ ∪ ( 𝐹 “ 𝐴 ) ∧ ( card ‘ ∪ ( 𝐹 “ 𝐴 ) ) = ∪ ( 𝐹 “ 𝐴 ) ) ) )
23 isinfcard ⊢ ( ( ω ⊆ ∪ ( 𝐹 “ 𝐴 ) ∧ ( card ‘ ∪ ( 𝐹 “ 𝐴 ) ) = ∪ ( 𝐹 “ 𝐴 ) ) ↔ ∪ ( 𝐹 “ 𝐴 ) ∈ ran ℵ )
24 22 23 syl6ib ⊢ ( 𝐴 ∈ V → ( ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) ∧ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ ) ) → ∪ ( 𝐹 “ 𝐴 ) ∈ ran ℵ ) )
25 24 exp4d ⊢ ( 𝐴 ∈ V → ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) → ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ → ∪ ( 𝐹 “ 𝐴 ) ∈ ran ℵ ) ) ) )
26 25 imp ⊢ ( ( 𝐴 ∈ V ∧ 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) ) → ( 𝑥 ∈ 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ → ∪ ( 𝐹 “ 𝐴 ) ∈ ran ℵ ) ) )
27 26 rexlimdv ⊢ ( ( 𝐴 ∈ V ∧ 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) ) → ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ → ∪ ( 𝐹 “ 𝐴 ) ∈ ran ℵ ) )
28 27 expimpd ⊢ ( 𝐴 ∈ V → ( ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) ∧ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ ) → ∪ ( 𝐹 “ 𝐴 ) ∈ ran ℵ ) )
29 1 28 syl ⊢ ( 𝐴 ∈ 𝐵 → ( ( 𝐹 : 𝐴 ⟶ ( ω ∪ ran ℵ ) ∧ ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ∈ ran ℵ ) → ∪ ( 𝐹 “ 𝐴 ) ∈ ran ℵ ) )