Metamath Proof Explorer


Theorem ipole

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

Ref Expression
Hypotheses ipoval.i I=toIncF
ipole.l ˙=I
Assertion ipole FVXFYFX˙YXY

Proof

Step Hyp Ref Expression
1 ipoval.i I=toIncF
2 ipole.l ˙=I
3 preq12 x=Xy=Yxy=XY
4 3 sseq1d x=Xy=YxyFXYF
5 sseq12 x=Xy=YxyXY
6 4 5 anbi12d x=Xy=YxyFxyXYFXY
7 eqid xy|xyFxy=xy|xyFxy
8 6 7 brabga XFYFXxy|xyFxyYXYFXY
9 8 3adant1 FVXFYFXxy|xyFxyYXYFXY
10 1 ipolerval FVxy|xyFxy=I
11 2 10 eqtr4id FV˙=xy|xyFxy
12 11 breqd FVX˙YXxy|xyFxyY
13 12 3ad2ant1 FVXFYFX˙YXxy|xyFxyY
14 prssi XFYFXYF
15 14 3adant1 FVXFYFXYF
16 15 biantrurd FVXFYFXYXYFXY
17 9 13 16 3bitr4d FVXFYFX˙YXY