This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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