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 𝐵 = ( Base ‘ 𝐾 )
pospo.l = ( le ‘ 𝐾 )
pospo.s < = ( lt ‘ 𝐾 )
Assertion pospo ( 𝐾𝑉 → ( 𝐾 ∈ Poset ↔ ( < Po 𝐵 ∧ ( I ↾ 𝐵 ) ⊆ ) ) )

Proof

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