Metamath Proof Explorer

Theorem numiunnum

Description: An indexed union of sets is numerable if its index set is numerable and there exists a collection of well-orderings on its members. (Contributed by Matthew House, 23-Aug-2025)

Ref Expression
Assertion numiunnum ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B → ⋃ x ∈ A B ∈ dom ⁡ card

Proof

Step Hyp Ref Expression
1 dfac8b ⊢ A ∈ dom ⁡ card → ∃ s s We A
2 1 adantr ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B → ∃ s s We A
3 simpll ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B ∧ s We A → A ∈ dom ⁡ card
4 simplr ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B ∧ s We A → ∀ x ∈ A B ∈ V ∧ S We B
5 r19.26 ⊢ ∀ x ∈ A B ∈ V ∧ S We B ↔ ∀ x ∈ A B ∈ V ∧ ∀ x ∈ A S We B
6 4 5 sylib ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B ∧ s We A → ∀ x ∈ A B ∈ V ∧ ∀ x ∈ A S We B
7 6 simpld ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B ∧ s We A → ∀ x ∈ A B ∈ V
8 iunexg ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V → ⋃ x ∈ A B ∈ V
9 3 7 8 syl2anc ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B ∧ s We A → ⋃ x ∈ A B ∈ V
10 9 9 xpexd ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B ∧ s We A → ⋃ x ∈ A B × ⋃ x ∈ A B ∈ V
11 opabssxp ⊢ y z | y ∈ ⋃ x ∈ A B ∧ z ∈ ⋃ x ∈ A B ∧ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y s w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∨ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∧ y ⦋ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y / x⦌ S z ⊆ ⋃ x ∈ A B × ⋃ x ∈ A B
12 11 a1i ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B ∧ s We A → y z | y ∈ ⋃ x ∈ A B ∧ z ∈ ⋃ x ∈ A B ∧ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y s w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∨ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∧ y ⦋ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y / x⦌ S z ⊆ ⋃ x ∈ A B × ⋃ x ∈ A B
13 10 12 ssexd ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B ∧ s We A → y z | y ∈ ⋃ x ∈ A B ∧ z ∈ ⋃ x ∈ A B ∧ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y s w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∨ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∧ y ⦋ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y / x⦌ S z ∈ V
14 simpr ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B ∧ s We A → s We A
15 exse ⊢ A ∈ dom ⁡ card → s Se A
16 15 ad2antrr ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B ∧ s We A → s Se A
17 6 simprd ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B ∧ s We A → ∀ x ∈ A S We B
18 eqid ⊢ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u
19 eqid ⊢ y z | y ∈ ⋃ x ∈ A B ∧ z ∈ ⋃ x ∈ A B ∧ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y s w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∨ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∧ y ⦋ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y / x⦌ S z = y z | y ∈ ⋃ x ∈ A B ∧ z ∈ ⋃ x ∈ A B ∧ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y s w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∨ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∧ y ⦋ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y / x⦌ S z
20 18 19 weiunwe ⊢ s We A ∧ s Se A ∧ ∀ x ∈ A S We B → y z | y ∈ ⋃ x ∈ A B ∧ z ∈ ⋃ x ∈ A B ∧ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y s w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∨ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∧ y ⦋ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y / x⦌ S z We ⋃ x ∈ A B
21 14 16 17 20 syl3anc ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B ∧ s We A → y z | y ∈ ⋃ x ∈ A B ∧ z ∈ ⋃ x ∈ A B ∧ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y s w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∨ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∧ y ⦋ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y / x⦌ S z We ⋃ x ∈ A B
22 weeq1 ⊢ t = y z | y ∈ ⋃ x ∈ A B ∧ z ∈ ⋃ x ∈ A B ∧ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y s w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∨ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∧ y ⦋ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y / x⦌ S z → t We ⋃ x ∈ A B ↔ y z | y ∈ ⋃ x ∈ A B ∧ z ∈ ⋃ x ∈ A B ∧ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y s w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∨ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y = w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ z ∧ y ⦋ w ∈ ⋃ x ∈ A B ⟼ ι u ∈ x ∈ A | w ∈ B | ∀ v ∈ x ∈ A | w ∈ B ¬ v s u ⁡ y / x⦌ S z We ⋃ x ∈ A B
23 13 21 22 spcedv ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B ∧ s We A → ∃ t t We ⋃ x ∈ A B
24 2 23 exlimddv ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B → ∃ t t We ⋃ x ∈ A B
25 ween ⊢ ⋃ x ∈ A B ∈ dom ⁡ card ↔ ∃ t t We ⋃ x ∈ A B
26 24 25 sylibr ⊢ A ∈ dom ⁡ card ∧ ∀ x ∈ A B ∈ V ∧ S We B → ⋃ x ∈ A B ∈ dom ⁡ card