Metamath Proof Explorer

Theorem resipos

Description: A set equipped with an order where no distinct elements are comparable is a poset. (Contributed by Zhi Wang, 20-Oct-2025)

Ref Expression
Hypothesis resipos.k ⊢ K = Base ndx B ≤ ndx I ↾ B
Assertion resipos ⊢ B ∈ V → K ∈ Poset

Proof

Step Hyp Ref Expression
1 resipos.k ⊢ K = Base ndx B ≤ ndx I ↾ B
2 prex ⊢ Base ndx B ≤ ndx I ↾ B ∈ V
3 1 2 eqeltri ⊢ K ∈ V
4 3 a1i ⊢ B ∈ V → K ∈ V
5 1 resiposbas ⊢ B ∈ V → B = Base K
6 resiexg ⊢ B ∈ V → I ↾ B ∈ V
7 basendxltplendx ⊢ Base ndx < ≤ ndx
8 plendxnn ⊢ ≤ ndx ∈ ℕ
9 pleid ⊢ le = Slot ≤ ndx
10 1 7 8 9 2strop ⊢ I ↾ B ∈ V → I ↾ B = ≤ K
11 6 10 syl ⊢ B ∈ V → I ↾ B = ≤ K
12 equid ⊢ x = x
13 resieq ⊢ x ∈ B ∧ x ∈ B → x I ↾ B x ↔ x = x
14 13 anidms ⊢ x ∈ B → x I ↾ B x ↔ x = x
15 12 14 mpbiri ⊢ x ∈ B → x I ↾ B x
16 15 adantl ⊢ B ∈ V ∧ x ∈ B → x I ↾ B x
17 resieq ⊢ x ∈ B ∧ y ∈ B → x I ↾ B y ↔ x = y
18 17 biimpd ⊢ x ∈ B ∧ y ∈ B → x I ↾ B y → x = y
19 18 adantrd ⊢ x ∈ B ∧ y ∈ B → x I ↾ B y ∧ y I ↾ B x → x = y
20 19 3adant1 ⊢ B ∈ V ∧ x ∈ B ∧ y ∈ B → x I ↾ B y ∧ y I ↾ B x → x = y
21 eqtr ⊢ x = y ∧ y = z → x = z
22 21 a1i ⊢ B ∈ V ∧ x ∈ B ∧ y ∈ B ∧ z ∈ B → x = y ∧ y = z → x = z
23 simpr1 ⊢ B ∈ V ∧ x ∈ B ∧ y ∈ B ∧ z ∈ B → x ∈ B
24 simpr2 ⊢ B ∈ V ∧ x ∈ B ∧ y ∈ B ∧ z ∈ B → y ∈ B
25 23 24 17 syl2anc ⊢ B ∈ V ∧ x ∈ B ∧ y ∈ B ∧ z ∈ B → x I ↾ B y ↔ x = y
26 simpr3 ⊢ B ∈ V ∧ x ∈ B ∧ y ∈ B ∧ z ∈ B → z ∈ B
27 resieq ⊢ y ∈ B ∧ z ∈ B → y I ↾ B z ↔ y = z
28 24 26 27 syl2anc ⊢ B ∈ V ∧ x ∈ B ∧ y ∈ B ∧ z ∈ B → y I ↾ B z ↔ y = z
29 25 28 anbi12d ⊢ B ∈ V ∧ x ∈ B ∧ y ∈ B ∧ z ∈ B → x I ↾ B y ∧ y I ↾ B z ↔ x = y ∧ y = z
30 resieq ⊢ x ∈ B ∧ z ∈ B → x I ↾ B z ↔ x = z
31 23 26 30 syl2anc ⊢ B ∈ V ∧ x ∈ B ∧ y ∈ B ∧ z ∈ B → x I ↾ B z ↔ x = z
32 22 29 31 3imtr4d ⊢ B ∈ V ∧ x ∈ B ∧ y ∈ B ∧ z ∈ B → x I ↾ B y ∧ y I ↾ B z → x I ↾ B z
33 4 5 11 16 20 32 isposd ⊢ B ∈ V → K ∈ Poset