Metamath Proof Explorer

Theorem iundom

Description: An upper bound for the cardinality of an indexed union. C depends on x and should be thought of as C ( x ) . (Contributed by NM, 26-Mar-2006)

Ref Expression
Assertion iundom ⊢ A ∈ V ∧ ∀ x ∈ A C ≼ B → ⋃ x ∈ A C ≼ A × B

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ x ∈ A x × C = ⋃ x ∈ A x × C
2 simpl ⊢ A ∈ V ∧ ∀ x ∈ A C ≼ B → A ∈ V
3 ovex ⊢ B C ∈ V
4 3 rgenw ⊢ ∀ x ∈ A B C ∈ V
5 iunexg ⊢ A ∈ V ∧ ∀ x ∈ A B C ∈ V → ⋃ x ∈ A B C ∈ V
6 2 4 5 sylancl ⊢ A ∈ V ∧ ∀ x ∈ A C ≼ B → ⋃ x ∈ A B C ∈ V
7 numth3 ⊢ ⋃ x ∈ A B C ∈ V → ⋃ x ∈ A B C ∈ dom ⁡ card
8 6 7 syl ⊢ A ∈ V ∧ ∀ x ∈ A C ≼ B → ⋃ x ∈ A B C ∈ dom ⁡ card
9 numacn ⊢ A ∈ V → ⋃ x ∈ A B C ∈ dom ⁡ card → ⋃ x ∈ A B C ∈ AC _ A
10 2 8 9 sylc ⊢ A ∈ V ∧ ∀ x ∈ A C ≼ B → ⋃ x ∈ A B C ∈ AC _ A
11 simpr ⊢ A ∈ V ∧ ∀ x ∈ A C ≼ B → ∀ x ∈ A C ≼ B
12 reldom ⊢ Rel ⁡ ≼
13 12 brrelex1i ⊢ C ≼ B → C ∈ V
14 13 ralimi ⊢ ∀ x ∈ A C ≼ B → ∀ x ∈ A C ∈ V
15 iunexg ⊢ A ∈ V ∧ ∀ x ∈ A C ∈ V → ⋃ x ∈ A C ∈ V
16 14 15 sylan2 ⊢ A ∈ V ∧ ∀ x ∈ A C ≼ B → ⋃ x ∈ A C ∈ V
17 1 10 11 iundom2g ⊢ A ∈ V ∧ ∀ x ∈ A C ≼ B → ⋃ x ∈ A x × C ≼ A × B
18 12 brrelex2i ⊢ ⋃ x ∈ A x × C ≼ A × B → A × B ∈ V
19 numth3 ⊢ A × B ∈ V → A × B ∈ dom ⁡ card
20 17 18 19 3syl ⊢ A ∈ V ∧ ∀ x ∈ A C ≼ B → A × B ∈ dom ⁡ card
21 numacn ⊢ ⋃ x ∈ A C ∈ V → A × B ∈ dom ⁡ card → A × B ∈ AC _ ⋃ x ∈ A C
22 16 20 21 sylc ⊢ A ∈ V ∧ ∀ x ∈ A C ≼ B → A × B ∈ AC _ ⋃ x ∈ A C
23 1 10 11 22 iundomg ⊢ A ∈ V ∧ ∀ x ∈ A C ≼ B → ⋃ x ∈ A C ≼ A × B