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

Metamath Proof Explorer

Theorem uniordint

Description: The union of a set of ordinals is equal to the intersection of its upper bounds. Problem 2.5(ii) of BellMachover p. 471. (Contributed by NM, 20-Sep-2003)

		Ref	Expression
	Hypothesis	uniordint.1	$⊢ A \in V$
	Assertion	uniordint	$⊢ A \subseteq On \to ⋃ A = ⋂ \{x \in On \| \forall y \in A y \subseteq x\}$

Proof

Step	Hyp	Ref	Expression
1		uniordint.1	$⊢ A \in V$
2	1	ssonunii	$⊢ A \subseteq On \to ⋃ A \in On$
3		intmin	$⊢ ⋃ A \in On \to ⋂ \{x \in On \| ⋃ A \subseteq x\} = ⋃ A$
4		unissb	$⊢ ⋃ A \subseteq x \leftrightarrow \forall y \in A y \subseteq x$
5	4	rabbii	$⊢ \{x \in On \| ⋃ A \subseteq x\} = \{x \in On \| \forall y \in A y \subseteq x\}$
6	5	inteqi	$⊢ ⋂ \{x \in On \| ⋃ A \subseteq x\} = ⋂ \{x \in On \| \forall y \in A y \subseteq x\}$
7	3 6	eqtr3di	$⊢ ⋃ A \in On \to ⋃ A = ⋂ \{x \in On \| \forall y \in A y \subseteq x\}$
8	2 7	syl	$⊢ A \subseteq On \to ⋃ A = ⋂ \{x \in On \| \forall y \in A y \subseteq x\}$