onmindif2

Description: The minimum of a class of ordinal numbers is less than the minimum of that class with its minimum removed. (Contributed by NM, 20-Nov-2003)

		Ref	Expression
	Assertion	onmindif2	$⊢ (A \subseteq On \land A \neq \emptyset) \to ⋂ A \in ⋂ (A ∖ \{⋂ A\})$

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$⊢ x \in (A ∖ \{⋂ A\}) \leftrightarrow (x \in A \land x \neq ⋂ A)$
2		onnmin	$⊢ (A \subseteq On \land x \in A) \to \neg x \in ⋂ A$
3	2	adantlr	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in A) \to \neg x \in ⋂ A$
4		oninton	$⊢ (A \subseteq On \land A \neq \emptyset) \to ⋂ A \in On$
5		ssel2	$⊢ (A \subseteq On \land x \in A) \to x \in On$
6	5	adantlr	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in A) \to x \in On$
7		ontri1	$⊢ (⋂ A \in On \land x \in On) \to (⋂ A \subseteq x \leftrightarrow \neg x \in ⋂ A)$
8		onsseleq	$⊢ (⋂ A \in On \land x \in On) \to (⋂ A \subseteq x \leftrightarrow (⋂ A \in x \lor ⋂ A = x))$
9	7 8	bitr3d	$⊢ (⋂ A \in On \land x \in On) \to (\neg x \in ⋂ A \leftrightarrow (⋂ A \in x \lor ⋂ A = x))$
10	4 6 9	syl2an2r	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in A) \to (\neg x \in ⋂ A \leftrightarrow (⋂ A \in x \lor ⋂ A = x))$
11	3 10	mpbid	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in A) \to (⋂ A \in x \lor ⋂ A = x)$
12	11	ord	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in A) \to (\neg ⋂ A \in x \to ⋂ A = x)$
13		eqcom	$⊢ ⋂ A = x \leftrightarrow x = ⋂ A$
14	12 13	imbitrdi	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in A) \to (\neg ⋂ A \in x \to x = ⋂ A)$
15	14	necon1ad	$⊢ ((A \subseteq On \land A \neq \emptyset) \land x \in A) \to (x \neq ⋂ A \to ⋂ A \in x)$
16	15	expimpd	$⊢ (A \subseteq On \land A \neq \emptyset) \to ((x \in A \land x \neq ⋂ A) \to ⋂ A \in x)$
17	1 16	biimtrid	$⊢ (A \subseteq On \land A \neq \emptyset) \to (x \in (A ∖ \{⋂ A\}) \to ⋂ A \in x)$
18	17	ralrimiv	$⊢ (A \subseteq On \land A \neq \emptyset) \to \forall x \in (A ∖ \{⋂ A\}) ⋂ A \in x$
19		intex	$⊢ A \neq \emptyset \leftrightarrow ⋂ A \in V$
20		elintg	$⊢ ⋂ A \in V \to (⋂ A \in ⋂ (A ∖ \{⋂ A\}) \leftrightarrow \forall x \in (A ∖ \{⋂ A\}) ⋂ A \in x)$
21	19 20	sylbi	$⊢ A \neq \emptyset \to (⋂ A \in ⋂ (A ∖ \{⋂ A\}) \leftrightarrow \forall x \in (A ∖ \{⋂ A\}) ⋂ A \in x)$
22	21	adantl	$⊢ (A \subseteq On \land A \neq \emptyset) \to (⋂ A \in ⋂ (A ∖ \{⋂ A\}) \leftrightarrow \forall x \in (A ∖ \{⋂ A\}) ⋂ A \in x)$
23	18 22	mpbird	$⊢ (A \subseteq On \land A \neq \emptyset) \to ⋂ A \in ⋂ (A ∖ \{⋂ A\})$

Metamath Proof Explorer

Theorem onmindif2

Proof