Metamath Proof Explorer

Theorem pospo

Description: Write a poset structure in terms of the proper-class poset predicate (strict less than version). (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses pospo.b ⊢B=BaseK
pospo.l ⊢≤˙=≤K
pospo.s ⊢<˙=<K
Assertion pospo ⊢K∈V→K∈Poset↔<˙PoB∧I↾B⊆≤˙

Proof

Step Hyp Ref Expression
1 pospo.b ⊢B=BaseK
2 pospo.l ⊢≤˙=≤K
3 pospo.s ⊢<˙=<K
4 3 pltirr ⊢K∈Poset∧x∈B→¬x<˙x
5 1 3 plttr ⊢K∈Poset∧x∈B∧y∈B∧z∈B→x<˙y∧y<˙z→x<˙z
6 4 5 ispod ⊢K∈Poset→<˙PoB
7 relres ⊢Rel⁡I↾B
8 7 a1i ⊢K∈Poset→Rel⁡I↾B
9 opabresid ⊢I↾B=xy|x∈B∧y=x
10 9 eqcomi ⊢xy|x∈B∧y=x=I↾B
11 10 eleq2i ⊢xy∈xy|x∈B∧y=x↔xy∈I↾B
12 opabidw ⊢xy∈xy|x∈B∧y=x↔x∈B∧y=x
13 11 12 bitr3i ⊢xy∈I↾B↔x∈B∧y=x
14 1 2 posref ⊢K∈Poset∧x∈B→x≤˙x
15 df-br ⊢x≤˙y↔xy∈≤˙
16 breq2 ⊢y=x→x≤˙y↔x≤˙x
17 15 16 bitr3id ⊢y=x→xy∈≤˙↔x≤˙x
18 14 17 syl5ibrcom ⊢K∈Poset∧x∈B→y=x→xy∈≤˙
19 18 expimpd ⊢K∈Poset→x∈B∧y=x→xy∈≤˙
20 13 19 biimtrid ⊢K∈Poset→xy∈I↾B→xy∈≤˙
21 8 20 relssdv ⊢K∈Poset→I↾B⊆≤˙
22 6 21 jca ⊢K∈Poset→<˙PoB∧I↾B⊆≤˙
23 simpl ⊢K∈V∧<˙PoB∧I↾B⊆≤˙→K∈V
24 1 a1i ⊢K∈V∧<˙PoB∧I↾B⊆≤˙→B=BaseK
25 2 a1i ⊢K∈V∧<˙PoB∧I↾B⊆≤˙→≤˙=≤K
26 equid ⊢x=x
27 simpr ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B→x∈B
28 resieq ⊢x∈B∧x∈B→xI↾Bx↔x=x
29 27 27 28 syl2anc ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B→xI↾Bx↔x=x
30 26 29 mpbiri ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B→xI↾Bx
31 simplrr ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B→I↾B⊆≤˙
32 31 ssbrd ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B→xI↾Bx→x≤˙x
33 30 32 mpd ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B→x≤˙x
34 1 2 3 pleval2i ⊢x∈B∧y∈B→x≤˙y→x<˙y∨x=y
35 34 3adant1 ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B→x≤˙y→x<˙y∨x=y
36 1 2 3 pleval2i ⊢y∈B∧x∈B→y≤˙x→y<˙x∨y=x
37 36 ancoms ⊢x∈B∧y∈B→y≤˙x→y<˙x∨y=x
38 37 3adant1 ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B→y≤˙x→y<˙x∨y=x
39 simprl ⊢K∈V∧<˙PoB∧I↾B⊆≤˙→<˙PoB
40 po2nr ⊢<˙PoB∧x∈B∧y∈B→¬x<˙y∧y<˙x
41 40 3impb ⊢<˙PoB∧x∈B∧y∈B→¬x<˙y∧y<˙x
42 39 41 syl3an1 ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B→¬x<˙y∧y<˙x
43 42 pm2.21d ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B→x<˙y∧y<˙x→x=y
44 simpl ⊢x=y∧y<˙x→x=y
45 44 a1i ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B→x=y∧y<˙x→x=y
46 simpr ⊢x<˙y∧y=x→y=x
47 46 equcomd ⊢x<˙y∧y=x→x=y
48 47 a1i ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B→x<˙y∧y=x→x=y
49 simpl ⊢x=y∧y=x→x=y
50 49 a1i ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B→x=y∧y=x→x=y
51 43 45 48 50 ccased ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B→x<˙y∨x=y∧y<˙x∨y=x→x=y
52 35 38 51 syl2and ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B→x≤˙y∧y≤˙x→x=y
53 simpr1 ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→x∈B
54 simpr2 ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→y∈B
55 53 54 34 syl2anc ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→x≤˙y→x<˙y∨x=y
56 simpr3 ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→z∈B
57 1 2 3 pleval2i ⊢y∈B∧z∈B→y≤˙z→y<˙z∨y=z
58 54 56 57 syl2anc ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→y≤˙z→y<˙z∨y=z
59 potr ⊢<˙PoB∧x∈B∧y∈B∧z∈B→x<˙y∧y<˙z→x<˙z
60 39 59 sylan ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→x<˙y∧y<˙z→x<˙z
61 simpll ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→K∈V
62 2 3 pltle ⊢K∈V∧x∈B∧z∈B→x<˙z→x≤˙z
63 61 53 56 62 syl3anc ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→x<˙z→x≤˙z
64 60 63 syld ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→x<˙y∧y<˙z→x≤˙z
65 breq1 ⊢x=y→x<˙z↔y<˙z
66 65 biimpar ⊢x=y∧y<˙z→x<˙z
67 66 63 syl5 ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→x=y∧y<˙z→x≤˙z
68 breq2 ⊢y=z→x<˙y↔x<˙z
69 68 biimpac ⊢x<˙y∧y=z→x<˙z
70 69 63 syl5 ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→x<˙y∧y=z→x≤˙z
71 53 33 syldan ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→x≤˙x
72 eqtr ⊢x=y∧y=z→x=z
73 72 breq2d ⊢x=y∧y=z→x≤˙x↔x≤˙z
74 71 73 syl5ibcom ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→x=y∧y=z→x≤˙z
75 64 67 70 74 ccased ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→x<˙y∨x=y∧y<˙z∨y=z→x≤˙z
76 55 58 75 syl2and ⊢K∈V∧<˙PoB∧I↾B⊆≤˙∧x∈B∧y∈B∧z∈B→x≤˙y∧y≤˙z→x≤˙z
77 23 24 25 33 52 76 isposd ⊢K∈V∧<˙PoB∧I↾B⊆≤˙→K∈Poset
78 77 ex ⊢K∈V→<˙PoB∧I↾B⊆≤˙→K∈Poset
79 22 78 impbid2 ⊢K∈V→K∈Poset↔<˙PoB∧I↾B⊆≤˙