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

Metamath Proof Explorer

Theorem uniimadomf

Description: An upper bound for the cardinality of the union of an image. Theorem 10.48 of TakeutiZaring p. 99. This version of uniimadom uses a bound-variable hypothesis in place of a distinct variable condition. (Contributed by NM, 26-Mar-2006)

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

Proof

Step Hyp Ref Expression
1 uniimadomf.1 ⊢ Ⅎ 𝑥 𝐹
2 uniimadomf.2 ⊢ 𝐴 ∈ V
3 uniimadomf.3 ⊢ 𝐵 ∈ V
4 nfv ⊢ Ⅎ 𝑧 ( 𝐹 ‘ 𝑥 ) ≼ 𝐵
5 nfcv ⊢ Ⅎ 𝑥 𝑧
6 1 5 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 )
7 nfcv ⊢ Ⅎ 𝑥 ≼
8 nfcv ⊢ Ⅎ 𝑥 𝐵
9 6 7 8 nfbr ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 ) ≼ 𝐵
10 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
11 10 breq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 ↔ ( 𝐹 ‘ 𝑧 ) ≼ 𝐵 ) )
12 4 9 11 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 ↔ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) ≼ 𝐵 )
13 2 3 uniimadom ⊢ ( ( Fun 𝐹 ∧ ∀ 𝑧 ∈ 𝐴 ( 𝐹 ‘ 𝑧 ) ≼ 𝐵 ) → ∪ ( 𝐹 “ 𝐴 ) ≼ ( 𝐴 × 𝐵 ) )
14 12 13 sylan2b ⊢ ( ( Fun 𝐹 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) ≼ 𝐵 ) → ∪ ( 𝐹 “ 𝐴 ) ≼ ( 𝐴 × 𝐵 ) )