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

Metamath Proof Explorer

Theorem unidom

Description: An upper bound for the cardinality of a union. Theorem 10.47 of TakeutiZaring p. 98. (Contributed by NM, 25-Mar-2006) (Proof shortened by Mario Carneiro, 1-Sep-2015)

		Ref	Expression
	Assertion	unidom	$⊢ (A \in V \land \forall x \in A x ≼ B) \to ⋃ A ≼ (A \times B)$

Proof

Step	Hyp	Ref	Expression
1		uniiun	$⊢ ⋃ A = ⋃_{x \in A} x$
2		iundom	$⊢ (A \in V \land \forall x \in A x ≼ B) \to ⋃_{x \in A} x ≼ (A \times B)$
3	1 2	eqbrtrid	$⊢ (A \in V \land \forall x \in A x ≼ B) \to ⋃ A ≼ (A \times B)$