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

Metamath Proof Explorer

Theorem iundomg

Description: An upper bound for the cardinality of an indexed union, with explicit choice principles. B depends on x and should be thought of as B ( x ) . (Contributed by Mario Carneiro, 1-Sep-2015)

Ref Expression
Hypotheses iunfo.1 ⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
iundomg.2 ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( 𝐶 ↑m 𝐵 ) ∈ AC 𝐴 )
iundomg.3 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ≼ 𝐶 )
iundomg.4 ⊢ ( 𝜑 → ( 𝐴 × 𝐶 ) ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 )
Assertion iundomg ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ ( 𝐴 × 𝐶 ) )

Proof

Step Hyp Ref Expression
1 iunfo.1 ⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
2 iundomg.2 ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( 𝐶 ↑m 𝐵 ) ∈ AC 𝐴 )
3 iundomg.3 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ≼ 𝐶 )
4 iundomg.4 ⊢ ( 𝜑 → ( 𝐴 × 𝐶 ) ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 )
5 1 2 3 iundom2g ⊢ ( 𝜑 → 𝑇 ≼ ( 𝐴 × 𝐶 ) )
6 acndom2 ⊢ ( 𝑇 ≼ ( 𝐴 × 𝐶 ) → ( ( 𝐴 × 𝐶 ) ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑇 ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 ) )
7 5 4 6 sylc ⊢ ( 𝜑 → 𝑇 ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 )
8 1 iunfo ⊢ ( 2nd ↾ 𝑇 ) : 𝑇 –onto→ ∪ 𝑥 ∈ 𝐴 𝐵
9 fodomacn ⊢ ( 𝑇 ∈ AC ∪ 𝑥 ∈ 𝐴 𝐵 → ( ( 2nd ↾ 𝑇 ) : 𝑇 –onto→ ∪ 𝑥 ∈ 𝐴 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ 𝑇 ) )
10 7 8 9 mpisyl ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ 𝑇 )
11 domtr ⊢ ( ( ∪ 𝑥 ∈ 𝐴 𝐵 ≼ 𝑇 ∧ 𝑇 ≼ ( 𝐴 × 𝐶 ) ) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ ( 𝐴 × 𝐶 ) )
12 10 5 11 syl2anc ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 ≼ ( 𝐴 × 𝐶 ) )