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

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 ⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ( I ↾ 𝐵 ) ⟩ }
Assertion resipos ( 𝐵 ∈ 𝑉 → 𝐾 ∈ Poset )

Proof

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