Theorem ipolt

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

	Ref	Expression
Hypotheses	ipolt.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
	ipolt.l	$$⊢\underset{\dot{}}{<}={<}_I$$
Assertion	ipolt	$$⊢\left(F\in V\wedge X\in F\wedge Y\in F\right)\to \left(X\underset{\dot{}}{<}Y\leftrightarrow X\subset Y\right)$$

Proof

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