Metamath Proof Explorer

Theorem isposd

Description: Properties that determine a poset (implicit structure version). (Contributed by Mario Carneiro, 29-Apr-2014) (Revised by AV, 26-Apr-2024)

Ref Expression
Hypotheses isposd.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
isposd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
isposd.l ⊢ ( 𝜑 → ≤ = ( le ‘ 𝐾 ) )
isposd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ≤ 𝑥 )
isposd.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) )
isposd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
Assertion isposd ( 𝜑 → 𝐾 ∈ Poset )

Proof

Step Hyp Ref Expression
1 isposd.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
2 isposd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
3 isposd.l ⊢ ( 𝜑 → ≤ = ( le ‘ 𝐾 ) )
4 isposd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ≤ 𝑥 )
5 isposd.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) )
6 isposd.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
7 1 elexd ⊢ ( 𝜑 → 𝐾 ∈ V )
8 4 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ≤ 𝑥 )
9 8 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑥 ≤ 𝑥 )
10 5 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) )
11 10 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) )
12 6 3exp2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 → ( 𝑧 ∈ 𝐵 → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) ) )
13 12 imp42 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
14 9 11 13 3jca ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) )
15 14 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) )
16 15 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) )
17 3 breqd ⊢ ( 𝜑 → ( 𝑥 ≤ 𝑥 ↔ 𝑥 ( le ‘ 𝐾 ) 𝑥 ) )
18 3 breqd ⊢ ( 𝜑 → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ( le ‘ 𝐾 ) 𝑦 ) )
19 3 breqd ⊢ ( 𝜑 → ( 𝑦 ≤ 𝑥 ↔ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) )
20 18 19 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ↔ ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) ) )
21 20 imbi1d ⊢ ( 𝜑 → ( ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
22 3 breqd ⊢ ( 𝜑 → ( 𝑦 ≤ 𝑧 ↔ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) )
23 18 22 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ↔ ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) ) )
24 3 breqd ⊢ ( 𝜑 → ( 𝑥 ≤ 𝑧 ↔ 𝑥 ( le ‘ 𝐾 ) 𝑧 ) )
25 23 24 imbi12d ⊢ ( 𝜑 → ( ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ↔ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
26 17 21 25 3anbi123d ⊢ ( 𝜑 → ( ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ↔ ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
27 2 26 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
28 2 27 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
29 2 28 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
30 29 anbi2d ⊢ ( 𝜑 → ( ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) ↔ ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) ) )
31 7 16 30 mpbi2and ⊢ ( 𝜑 → ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
32 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
33 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
34 32 33 ispos ⊢ ( 𝐾 ∈ Poset ↔ ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
35 31 34 sylibr ⊢ ( 𝜑 → 𝐾 ∈ Poset )