ipolt

Description: Strict order condition of the inclusion poset. (Contributed by Stefan O'Rear, 30-Jan-2015)

	Ref	Expression
Hypotheses	ipolt.i	$⊢ I = toInc (F)$
	ipolt.l	$⊢ \underset{˙}{<} = <_{I}$
Assertion	ipolt	$⊢ (F \in V \land X \in F \land Y \in F) \to (X \underset{˙}{<} Y \leftrightarrow X \subset Y)$

Step	Hyp	Ref	Expression
1		ipolt.i	$⊢ I = toInc (F)$
2		ipolt.l	$⊢ \underset{˙}{<} = <_{I}$
3		eqid	$⊢ \leq_{I} = \leq_{I}$
4	1 3	ipole	$⊢ (F \in V \land X \in F \land Y \in F) \to (X \leq_{I} Y \leftrightarrow X \subseteq Y)$
5	4	anbi1d	$⊢ (F \in V \land X \in F \land Y \in F) \to ((X \leq_{I} Y \land X \neq Y) \leftrightarrow (X \subseteq Y \land X \neq Y))$
6	1	fvexi	$⊢ I \in V$
7	3 2	pltval	$⊢ (I \in V \land X \in F \land Y \in F) \to (X \underset{˙}{<} Y \leftrightarrow (X \leq_{I} Y \land X \neq Y))$
8	6 7	mp3an1	$⊢ (X \in F \land Y \in F) \to (X \underset{˙}{<} Y \leftrightarrow (X \leq_{I} Y \land X \neq Y))$
9	8	3adant1	$⊢ (F \in V \land X \in F \land Y \in F) \to (X \underset{˙}{<} Y \leftrightarrow (X \leq_{I} Y \land X \neq Y))$
10		df-pss	$⊢ X \subset Y \leftrightarrow (X \subseteq Y \land X \neq Y)$
11	10	a1i	$⊢ (F \in V \land X \in F \land Y \in F) \to (X \subset Y \leftrightarrow (X \subseteq Y \land X \neq Y))$
12	5 9 11	3bitr4d	$⊢ (F \in V \land X \in F \land Y \in F) \to (X \underset{˙}{<} Y \leftrightarrow X \subset Y)$

Metamath Proof Explorer