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 ⊢ A ≼ ω ∧ ∀ x ∈ A B ≼ ω → ⋃ x ∈ A B ≼ ω

Proof

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