Theorem ipole

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

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

Proof

Step	Hyp	Ref	Expression
1		ipoval.i	$$⊢I=\mathrm{toInc}\left(F\right)$$
2		ipole.l	$$⊢\underset{\dot{}}{\le }={\le }_I$$
3		preq12	$$⊢\left(x=X\wedge y=Y\right)\to \left\{x,y\right\}=\left\{X,Y\right\}$$
4	3	sseq1d	$$⊢\left(x=X\wedge y=Y\right)\to \left(\left\{x,y\right\}\subseteq F\leftrightarrow \left\{X,Y\right\}\subseteq F\right)$$
5		sseq12	$$⊢\left(x=X\wedge y=Y\right)\to \left(x\subseteq y\leftrightarrow X\subseteq Y\right)$$
6	4 5	anbi12d	$$⊢\left(x=X\wedge y=Y\right)\to \left(\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\leftrightarrow \left(\left\{X,Y\right\}\subseteq F\wedge X\subseteq Y\right)\right)$$
7		eqid	$$⊢\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}$$
8	6 7	brabga	$$⊢\left(X\in F\wedge Y\in F\right)\to \left(X\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}Y\leftrightarrow \left(\left\{X,Y\right\}\subseteq F\wedge X\subseteq Y\right)\right)$$
9	8	3adant1	$$⊢\left(F\in V\wedge X\in F\wedge Y\in F\right)\to \left(X\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}Y\leftrightarrow \left(\left\{X,Y\right\}\subseteq F\wedge X\subseteq Y\right)\right)$$
10	1	ipolerval	$$⊢F\in V\to \left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}={\le }_I$$
11	2 10	eqtr4id	$$⊢F\in V\to \underset{\dot{}}{\le }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}$$
12	11	breqd	$$⊢F\in V\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow X\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}Y\right)$$
13	12	3ad2ant1	$$⊢\left(F\in V\wedge X\in F\wedge Y\in F\right)\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow X\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq F\wedge x\subseteq y\right)\right\}Y\right)$$
14		prssi	$$⊢\left(X\in F\wedge Y\in F\right)\to \left\{X,Y\right\}\subseteq F$$
15	14	3adant1	$$⊢\left(F\in V\wedge X\in F\wedge Y\in F\right)\to \left\{X,Y\right\}\subseteq F$$
16	15	biantrurd	$$⊢\left(F\in V\wedge X\in F\wedge Y\in F\right)\to \left(X\subseteq Y\leftrightarrow \left(\left\{X,Y\right\}\subseteq F\wedge X\subseteq Y\right)\right)$$
17	9 13 16	3bitr4d	$$⊢\left(F\in V\wedge X\in F\wedge Y\in F\right)\to \left(X\underset{\dot{}}{\le }Y\leftrightarrow X\subseteq Y\right)$$