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