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 ⊢ Ⅎ _ x F
uniimadomf.2 ⊢ A ∈ V
uniimadomf.3 ⊢ B ∈ V
Assertion uniimadomf ⊢ Fun ⁡ F ∧ ∀ x ∈ A F ⁡ x ≼ B → ⋃ F A ≼ A × B

Proof

Step Hyp Ref Expression
1 uniimadomf.1 ⊢ Ⅎ _ x F
2 uniimadomf.2 ⊢ A ∈ V
3 uniimadomf.3 ⊢ B ∈ V
4 nfv ⊢ Ⅎ z F ⁡ x ≼ B
5 nfcv ⊢ Ⅎ _ x z
6 1 5 nffv ⊢ Ⅎ _ x F ⁡ z
7 nfcv ⊢ Ⅎ _ x ≼
8 nfcv ⊢ Ⅎ _ x B
9 6 7 8 nfbr ⊢ Ⅎ x F ⁡ z ≼ B
10 fveq2 ⊢ x = z → F ⁡ x = F ⁡ z
11 10 breq1d ⊢ x = z → F ⁡ x ≼ B ↔ F ⁡ z ≼ B
12 4 9 11 cbvralw ⊢ ∀ x ∈ A F ⁡ x ≼ B ↔ ∀ z ∈ A F ⁡ z ≼ B
13 2 3 uniimadom ⊢ Fun ⁡ F ∧ ∀ z ∈ A F ⁡ z ≼ B → ⋃ F A ≼ A × B
14 12 13 sylan2b ⊢ Fun ⁡ F ∧ ∀ x ∈ A F ⁡ x ≼ B → ⋃ F A ≼ A × B