This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid ⊢ ( 𝐾 ∈ 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 ↾ 𝐵 ) ⊆ ≤ ) ) )