iunctb

Description: The countable union of countable sets is countable (indexed union version of unictb ). (Contributed by Mario Carneiro, 18-Jan-2014)

		Ref	Expression
	Assertion	iunctb	$⊢ (A ≼ ω \land \forall x \in A B ≼ ω) \to ⋃_{x \in A} B ≼ ω$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ⋃_{x \in A} (\{x\} \times B) = ⋃_{x \in A} (\{x\} \times B)$
2		simpl	$⊢ (A ≼ ω \land \forall x \in A B ≼ ω) \to A ≼ ω$
3		ctex	$⊢ A ≼ ω \to A \in V$
4	3	adantr	$⊢ (A ≼ ω \land \forall x \in A B ≼ ω) \to A \in V$
5		ovex	$⊢ ω^{B} \in V$
6	5	rgenw	$⊢ \forall x \in A ω^{B} \in V$
7		iunexg	$⊢ (A \in V \land \forall x \in A ω^{B} \in V) \to ⋃_{x \in A} (ω^{B}) \in V$
8	4 6 7	sylancl	$⊢ (A ≼ ω \land \forall x \in A B ≼ ω) \to ⋃_{x \in A} (ω^{B}) \in V$
9		acncc	$⊢ \underline{AC} ω = V$
10	8 9	eleqtrrdi	$⊢ (A ≼ ω \land \forall x \in A B ≼ ω) \to ⋃_{x \in A} (ω^{B}) \in \underline{AC} ω$
11		acndom	$⊢ A ≼ ω \to (⋃_{x \in A} (ω^{B}) \in \underline{AC} ω \to ⋃_{x \in A} (ω^{B}) \in \underline{AC} A)$
12	2 10 11	sylc	$⊢ (A ≼ ω \land \forall x \in A B ≼ ω) \to ⋃_{x \in A} (ω^{B}) \in \underline{AC} A$
13		simpr	$⊢ (A ≼ ω \land \forall x \in A B ≼ ω) \to \forall x \in A B ≼ ω$
14		omex	$⊢ ω \in V$
15		xpdom1g	$⊢ (ω \in V \land A ≼ ω) \to (A \times ω) ≼ (ω \times ω)$
16	14 2 15	sylancr	$⊢ (A ≼ ω \land \forall x \in A B ≼ ω) \to (A \times ω) ≼ (ω \times ω)$
17		xpomen	$⊢ (ω \times ω) \approx ω$
18		domentr	$⊢ ((A \times ω) ≼ (ω \times ω) \land (ω \times ω) \approx ω) \to (A \times ω) ≼ ω$
19	16 17 18	sylancl	$⊢ (A ≼ ω \land \forall x \in A B ≼ ω) \to (A \times ω) ≼ ω$
20		ctex	$⊢ B ≼ ω \to B \in V$
21	20	ralimi	$⊢ \forall x \in A B ≼ ω \to \forall x \in A B \in V$
22		iunexg	$⊢ (A \in V \land \forall x \in A B \in V) \to ⋃_{x \in A} B \in V$
23	3 21 22	syl2an	$⊢ (A ≼ ω \land \forall x \in A B ≼ ω) \to ⋃_{x \in A} B \in V$
24		omelon	$⊢ ω \in On$
25		onenon	$⊢ ω \in On \to ω \in dom card$
26	24 25	ax-mp	$⊢ ω \in dom card$
27		numacn	$⊢ ⋃_{x \in A} B \in V \to (ω \in dom card \to ω \in \underline{AC} ⋃_{x \in A} B)$
28	23 26 27	mpisyl	$⊢ (A ≼ ω \land \forall x \in A B ≼ ω) \to ω \in \underline{AC} ⋃_{x \in A} B$
29		acndom2	$⊢ (A \times ω) ≼ ω \to (ω \in \underline{AC} ⋃_{x \in A} B \to A \times ω \in \underline{AC} ⋃_{x \in A} B)$
30	19 28 29	sylc	$⊢ (A ≼ ω \land \forall x \in A B ≼ ω) \to A \times ω \in \underline{AC} ⋃_{x \in A} B$
31	1 12 13 30	iundomg	$⊢ (A ≼ ω \land \forall x \in A B ≼ ω) \to ⋃_{x \in A} B ≼ (A \times ω)$
32		domtr	$⊢ (⋃_{x \in A} B ≼ (A \times ω) \land (A \times ω) ≼ ω) \to ⋃_{x \in A} B ≼ ω$
33	31 19 32	syl2anc	$⊢ (A ≼ ω \land \forall x \in A B ≼ ω) \to ⋃_{x \in A} B ≼ ω$

Metamath Proof Explorer

Theorem iunctb

Proof