Theorem 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	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω ) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ ω )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
2		simpl	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω ) → 𝐴 ≼ ω )
3		ctex	⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V )
4	3	adantr	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω ) → 𝐴 ∈ V )
5		ovex	⊢ ( ω ↑m 𝐵 ) ∈ V
6	5	rgenw	⊢ ∀ 𝑥 ∈ 𝐴 ( ω ↑m 𝐵 ) ∈ V
7		iunexg	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 ( ω ↑m 𝐵 ) ∈ V ) → ∪ 𝑥 ∈ 𝐴 ( ω ↑m 𝐵 ) ∈ V )
8	4 6 7	sylancl	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω ) → ∪ 𝑥 ∈ 𝐴 ( ω ↑m 𝐵 ) ∈ V )
9		acncc	⊢ AC ω = V
10	8 9	eleqtrrdi	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω ) → ∪ 𝑥 ∈ 𝐴 ( ω ↑m 𝐵 ) ∈ AC ω )
11		acndom	⊢ ( 𝐴 ≼ ω → ( ∪ 𝑥 ∈ 𝐴 ( ω ↑m 𝐵 ) ∈ AC ω → ∪ 𝑥 ∈ 𝐴 ( ω ↑m 𝐵 ) ∈ AC 𝐴 ) )
12	2 10 11	sylc	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω ) → ∪ 𝑥 ∈ 𝐴 ( ω ↑m 𝐵 ) ∈ AC 𝐴 )
13		simpr	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω ) → ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω )
14		omex	⊢ ω ∈ V
15		xpdom1g	⊢ ( ( ω ∈ V ∧ 𝐴 ≼ ω ) → ( 𝐴 × ω ) ≼ ( ω × ω ) )
16	14 2 15	sylancr	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω ) → ( 𝐴 × ω ) ≼ ( ω × ω ) )
17		xpomen	⊢ ( ω × ω ) ≈ ω
18		domentr	⊢ ( ( ( 𝐴 × ω ) ≼ ( ω × ω ) ∧ ( ω × ω ) ≈ ω ) → ( 𝐴 × ω ) ≼ ω )
19	16 17 18	sylancl	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω ) → ( 𝐴 × ω ) ≼ ω )
20		ctex	⊢ ( 𝐵 ≼ ω → 𝐵 ∈ V )
21	20	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V )
22		iunexg	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
23	3 21 22	syl2an	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
24		omelon	⊢ ω ∈ On
25		onenon	⊢ ( ω ∈ On → ω ∈ dom card )
26	24 25	ax-mp	⊢ ω ∈ dom card
27		numacn	⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V → ( ω ∈ dom card → ω ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 ) )
28	23 26 27	mpisyl	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω ) → ω ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 )
29		acndom2	⊢ ( ( 𝐴 × ω ) ≼ ω → ( ω ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 → ( 𝐴 × ω ) ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 ) )
30	19 28 29	sylc	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω ) → ( 𝐴 × ω ) ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 )
31	1 12 13 30	iundomg	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω ) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ ( 𝐴 × ω ) )
32		domtr	⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ≼ ( 𝐴 × ω ) ∧ ( 𝐴 × ω ) ≼ ω ) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ ω )
33	31 19 32	syl2anc	⊢ ( ( 𝐴 ≼ ω ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ≼ ω ) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ ω )