Theorem 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	|- .< = ( lt ` I )
Assertion	ipolt	|- ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X .< Y <-> X C. Y ) )

Proof

Step	Hyp	Ref	Expression
1		ipolt.i	|- I = ( toInc ` F )
2		ipolt.l	|- .< = ( lt ` I )
3		eqid	|- ( le ` I ) = ( le ` I )
4	1 3	ipole	|- ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X ( le ` I ) Y <-> X C_ Y ) )
5	4	anbi1d	|- ( ( F e. V /\ X e. F /\ Y e. F ) -> ( ( X ( le ` I ) Y /\ X =/= Y ) <-> ( X C_ Y /\ X =/= Y ) ) )
6	1	fvexi	|- I e. _V
7	3 2	pltval	|- ( ( I e. _V /\ X e. F /\ Y e. F ) -> ( X .< Y <-> ( X ( le ` I ) Y /\ X =/= Y ) ) )
8	6 7	mp3an1	|- ( ( X e. F /\ Y e. F ) -> ( X .< Y <-> ( X ( le ` I ) Y /\ X =/= Y ) ) )
9	8	3adant1	|- ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X .< Y <-> ( X ( le ` I ) Y /\ X =/= Y ) ) )
10		df-pss	|- ( X C. Y <-> ( X C_ Y /\ X =/= Y ) )
11	10	a1i	|- ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X C. Y <-> ( X C_ Y /\ X =/= Y ) ) )
12	5 9 11	3bitr4d	|- ( ( F e. V /\ X e. F /\ Y e. F ) -> ( X .< Y <-> X C. Y ) )