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

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 ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 𝐶 ≼ ( 𝐴 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐶 ) = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐶 )
2 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → 𝐴 ∈ 𝑉 )
3 ovex ⊢ ( 𝐵 ↑m 𝐶 ) ∈ V
4 3 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ V
5 iunexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ V ) → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ V )
6 2 4 5 sylancl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ V )
7 numth3 ⊢ ( ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ V → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ dom card )
8 6 7 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ dom card )
9 numacn ⊢ ( 𝐴 ∈ 𝑉 → ( ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ dom card → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ AC 𝐴 ) )
10 2 8 9 sylc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 ( 𝐵 ↑m 𝐶 ) ∈ AC 𝐴 )
11 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 )
12 reldom ⊢ Rel ≼
13 12 brrelex1i ⊢ ( 𝐶 ≼ 𝐵 → 𝐶 ∈ V )
14 13 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 → ∀ 𝑥 ∈ 𝐴 𝐶 ∈ V )
15 iunexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ∈ V ) → ∪ 𝑥 ∈ 𝐴 𝐶 ∈ V )
16 14 15 sylan2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 𝐶 ∈ V )
17 1 10 11 iundom2g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐶 ) ≼ ( 𝐴 × 𝐵 ) )
18 12 brrelex2i ⊢ ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐶 ) ≼ ( 𝐴 × 𝐵 ) → ( 𝐴 × 𝐵 ) ∈ V )
19 numth3 ⊢ ( ( 𝐴 × 𝐵 ) ∈ V → ( 𝐴 × 𝐵 ) ∈ dom card )
20 17 18 19 3syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ( 𝐴 × 𝐵 ) ∈ dom card )
21 numacn ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐶 ∈ V → ( ( 𝐴 × 𝐵 ) ∈ dom card → ( 𝐴 × 𝐵 ) ∈ AC ∪ 𝑥 ∈ 𝐴 𝐶 ) )
22 16 20 21 sylc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ( 𝐴 × 𝐵 ) ∈ AC ∪ 𝑥 ∈ 𝐴 𝐶 )
23 1 10 11 22 iundomg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 ≼ 𝐵 ) → ∪ 𝑥 ∈ 𝐴 𝐶 ≼ ( 𝐴 × 𝐵 ) )