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

Metamath Proof Explorer

Theorem uniimadom

Description: An upper bound for the cardinality of the union of an image. Theorem 10.48 of TakeutiZaring p. 99. (Contributed by NM, 25-Mar-2006)

Ref Expression
Hypotheses uniimadom.1 ⊢ 𝐴 ∈ V
uniimadom.2 ⊢ 𝐵 ∈ V
Assertion uniimadom ( ( Fun 𝐹 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 ) → ∪ ( 𝐹 “ 𝐴 ) ≼ ( 𝐴 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 uniimadom.1 ⊢ 𝐴 ∈ V
2 uniimadom.2 ⊢ 𝐵 ∈ V
3 1 funimaex ⊢ ( Fun 𝐹 → ( 𝐹 “ 𝐴 ) ∈ V )
4 3 adantr ⊢ ( ( Fun 𝐹 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 ) → ( 𝐹 “ 𝐴 ) ∈ V )
5 fvelima ⊢ ( ( Fun 𝐹 ∧ 𝑦 ∈ ( 𝐹 “ 𝐴 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 )
6 5 ex ⊢ ( Fun 𝐹 → ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 ) )
7 breq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 ↔ 𝑦 ≼ 𝐵 ) )
8 7 biimpd ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 → 𝑦 ≼ 𝐵 ) )
9 8 reximi ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 → ∃ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 → 𝑦 ≼ 𝐵 ) )
10 r19.36v ⊢ ( ∃ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 → 𝑦 ≼ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 → 𝑦 ≼ 𝐵 ) )
11 9 10 syl ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = 𝑦 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 → 𝑦 ≼ 𝐵 ) )
12 6 11 syl6 ⊢ ( Fun 𝐹 → ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 → 𝑦 ≼ 𝐵 ) ) )
13 12 com23 ⊢ ( Fun 𝐹 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 → ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) → 𝑦 ≼ 𝐵 ) ) )
14 13 imp ⊢ ( ( Fun 𝐹 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 ) → ( 𝑦 ∈ ( 𝐹 “ 𝐴 ) → 𝑦 ≼ 𝐵 ) )
15 14 ralrimiv ⊢ ( ( Fun 𝐹 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 ) → ∀ 𝑦 ∈ ( 𝐹 “ 𝐴 ) 𝑦 ≼ 𝐵 )
16 unidom ⊢ ( ( ( 𝐹 “ 𝐴 ) ∈ V ∧ ∀ 𝑦 ∈ ( 𝐹 “ 𝐴 ) 𝑦 ≼ 𝐵 ) → ∪ ( 𝐹 “ 𝐴 ) ≼ ( ( 𝐹 “ 𝐴 ) × 𝐵 ) )
17 4 15 16 syl2anc ⊢ ( ( Fun 𝐹 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 ) → ∪ ( 𝐹 “ 𝐴 ) ≼ ( ( 𝐹 “ 𝐴 ) × 𝐵 ) )
18 imadomg ⊢ ( 𝐴 ∈ V → ( Fun 𝐹 → ( 𝐹 “ 𝐴 ) ≼ 𝐴 ) )
19 1 18 ax-mp ⊢ ( Fun 𝐹 → ( 𝐹 “ 𝐴 ) ≼ 𝐴 )
20 2 xpdom1 ⊢ ( ( 𝐹 “ 𝐴 ) ≼ 𝐴 → ( ( 𝐹 “ 𝐴 ) × 𝐵 ) ≼ ( 𝐴 × 𝐵 ) )
21 19 20 syl ⊢ ( Fun 𝐹 → ( ( 𝐹 “ 𝐴 ) × 𝐵 ) ≼ ( 𝐴 × 𝐵 ) )
22 21 adantr ⊢ ( ( Fun 𝐹 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 ) → ( ( 𝐹 “ 𝐴 ) × 𝐵 ) ≼ ( 𝐴 × 𝐵 ) )
23 domtr ⊢ ( ( ∪ ( 𝐹 “ 𝐴 ) ≼ ( ( 𝐹 “ 𝐴 ) × 𝐵 ) ∧ ( ( 𝐹 “ 𝐴 ) × 𝐵 ) ≼ ( 𝐴 × 𝐵 ) ) → ∪ ( 𝐹 “ 𝐴 ) ≼ ( 𝐴 × 𝐵 ) )
24 17 22 23 syl2anc ⊢ ( ( Fun 𝐹 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 ) → ∪ ( 𝐹 “ 𝐴 ) ≼ ( 𝐴 × 𝐵 ) )