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	$⊢ A \in B \to ((F : A ⟶ ω \cup ran ℵ \land \exists x \in A F (x) \in ran ℵ) \to ⋃ F [A] \in ran ℵ)$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in B \to A \in V$
2		isinfcard	$⊢ (ω \subseteq F (x) \land card (F (x)) = F (x)) \leftrightarrow F (x) \in ran ℵ$
3	2	bicomi	$⊢ F (x) \in ran ℵ \leftrightarrow (ω \subseteq F (x) \land card (F (x)) = F (x))$
4	3	simplbi	$⊢ F (x) \in ran ℵ \to ω \subseteq F (x)$
5		ffn	$⊢ F : A ⟶ ω \cup ran ℵ \to F Fn A$
6		fnfvelrn	$⊢ (F Fn A \land x \in A) \to F (x) \in ran F$
7	6	ex	$⊢ F Fn A \to (x \in A \to F (x) \in ran F)$
8		fnima	$⊢ F Fn A \to F [A] = ran F$
9	8	eleq2d	$⊢ F Fn A \to (F (x) \in F [A] \leftrightarrow F (x) \in ran F)$
10	7 9	sylibrd	$⊢ F Fn A \to (x \in A \to F (x) \in F [A])$
11		elssuni	$⊢ F (x) \in F [A] \to F (x) \subseteq ⋃ F [A]$
12	10 11	syl6	$⊢ F Fn A \to (x \in A \to F (x) \subseteq ⋃ F [A])$
13	12	imp	$⊢ (F Fn A \land x \in A) \to F (x) \subseteq ⋃ F [A]$
14	5 13	sylan	$⊢ (F : A ⟶ ω \cup ran ℵ \land x \in A) \to F (x) \subseteq ⋃ F [A]$
15	4 14	sylan9ssr	$⊢ ((F : A ⟶ ω \cup ran ℵ \land x \in A) \land F (x) \in ran ℵ) \to ω \subseteq ⋃ F [A]$
16	15	anasss	$⊢ (F : A ⟶ ω \cup ran ℵ \land (x \in A \land F (x) \in ran ℵ)) \to ω \subseteq ⋃ F [A]$
17	16	a1i	$⊢ A \in V \to ((F : A ⟶ ω \cup ran ℵ \land (x \in A \land F (x) \in ran ℵ)) \to ω \subseteq ⋃ F [A])$
18		carduniima	$⊢ A \in V \to (F : A ⟶ ω \cup ran ℵ \to ⋃ F [A] \in (ω \cup ran ℵ))$
19		iscard3	$⊢ card (⋃ F [A]) = ⋃ F [A] \leftrightarrow ⋃ F [A] \in (ω \cup ran ℵ)$
20	18 19	imbitrrdi	$⊢ A \in V \to (F : A ⟶ ω \cup ran ℵ \to card (⋃ F [A]) = ⋃ F [A])$
21	20	adantrd	$⊢ A \in V \to ((F : A ⟶ ω \cup ran ℵ \land (x \in A \land F (x) \in ran ℵ)) \to card (⋃ F [A]) = ⋃ F [A])$
22	17 21	jcad	$⊢ A \in V \to ((F : A ⟶ ω \cup ran ℵ \land (x \in A \land F (x) \in ran ℵ)) \to (ω \subseteq ⋃ F [A] \land card (⋃ F [A]) = ⋃ F [A]))$
23		isinfcard	$⊢ (ω \subseteq ⋃ F [A] \land card (⋃ F [A]) = ⋃ F [A]) \leftrightarrow ⋃ F [A] \in ran ℵ$
24	22 23	imbitrdi	$⊢ A \in V \to ((F : A ⟶ ω \cup ran ℵ \land (x \in A \land F (x) \in ran ℵ)) \to ⋃ F [A] \in ran ℵ)$
25	24	exp4d	$⊢ A \in V \to (F : A ⟶ ω \cup ran ℵ \to (x \in A \to (F (x) \in ran ℵ \to ⋃ F [A] \in ran ℵ)))$
26	25	imp	$⊢ (A \in V \land F : A ⟶ ω \cup ran ℵ) \to (x \in A \to (F (x) \in ran ℵ \to ⋃ F [A] \in ran ℵ))$
27	26	rexlimdv	$⊢ (A \in V \land F : A ⟶ ω \cup ran ℵ) \to (\exists x \in A F (x) \in ran ℵ \to ⋃ F [A] \in ran ℵ)$
28	27	expimpd	$⊢ A \in V \to ((F : A ⟶ ω \cup ran ℵ \land \exists x \in A F (x) \in ran ℵ) \to ⋃ F [A] \in ran ℵ)$
29	1 28	syl	$⊢ A \in B \to ((F : A ⟶ ω \cup ran ℵ \land \exists x \in A F (x) \in ran ℵ) \to ⋃ F [A] \in ran ℵ)$

Metamath Proof Explorer

Theorem cardinfima

Proof