Metamath Proof Explorer

Theorem dfom5b

Description: A quantifier-free definition of _om that does not depend on ax-inf . (Note: label was changed from dfom5 to dfom5b to prevent naming conflict. NM, 12-Feb-2013.) (Contributed by Scott Fenton, 11-Apr-2012)

		Ref	Expression
	Assertion	dfom5b	$⊢ ω = On \cap ⋂ 𝖫𝗂𝗆𝗂𝗍𝗌$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2	1	elint	$⊢ x \in ⋂ 𝖫𝗂𝗆𝗂𝗍𝗌 \leftrightarrow \forall y (y \in 𝖫𝗂𝗆𝗂𝗍𝗌 \to x \in y)$
3		vex	$⊢ y \in V$
4	3	ellimits	$⊢ y \in 𝖫𝗂𝗆𝗂𝗍𝗌 \leftrightarrow Lim y$
5	4	imbi1i	$⊢ (y \in 𝖫𝗂𝗆𝗂𝗍𝗌 \to x \in y) \leftrightarrow (Lim y \to x \in y)$
6	5	albii	$⊢ \forall y (y \in 𝖫𝗂𝗆𝗂𝗍𝗌 \to x \in y) \leftrightarrow \forall y (Lim y \to x \in y)$
7	2 6	bitr2i	$⊢ \forall y (Lim y \to x \in y) \leftrightarrow x \in ⋂ 𝖫𝗂𝗆𝗂𝗍𝗌$
8	7	anbi2i	$⊢ (x \in On \land \forall y (Lim y \to x \in y)) \leftrightarrow (x \in On \land x \in ⋂ 𝖫𝗂𝗆𝗂𝗍𝗌)$
9		elom	$⊢ x \in ω \leftrightarrow (x \in On \land \forall y (Lim y \to x \in y))$
10		elin	$⊢ x \in (On \cap ⋂ 𝖫𝗂𝗆𝗂𝗍𝗌) \leftrightarrow (x \in On \land x \in ⋂ 𝖫𝗂𝗆𝗂𝗍𝗌)$
11	8 9 10	3bitr4i	$⊢ x \in ω \leftrightarrow x \in (On \cap ⋂ 𝖫𝗂𝗆𝗂𝗍𝗌)$
12	11	eqriv	$⊢ ω = On \cap ⋂ 𝖫𝗂𝗆𝗂𝗍𝗌$