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

Metamath Proof Explorer

Theorem isprsd

Description: Property of being a preordered set (deduction form). (Contributed by Zhi Wang, 18-Sep-2024)

Ref Expression
Hypotheses isprsd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
isprsd.l ⊢ ( 𝜑 → ≤ = ( le ‘ 𝐾 ) )
isprsd.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
Assertion isprsd ( 𝜑 → ( 𝐾 ∈ Proset ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )

Proof

Step Hyp Ref Expression
1 isprsd.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2 isprsd.l ⊢ ( 𝜑 → ≤ = ( le ‘ 𝐾 ) )
3 isprsd.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
4 3 elexd ⊢ ( 𝜑 → 𝐾 ∈ V )
5 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7 5 6 isprs ⊢ ( 𝐾 ∈ Proset ↔ ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
8 7 baib ⊢ ( 𝐾 ∈ V → ( 𝐾 ∈ Proset ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
9 4 8 syl ⊢ ( 𝜑 → ( 𝐾 ∈ Proset ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
10 2 breqd ⊢ ( 𝜑 → ( 𝑥 ≤ 𝑥 ↔ 𝑥 ( le ‘ 𝐾 ) 𝑥 ) )
11 2 breqd ⊢ ( 𝜑 → ( 𝑥 ≤ 𝑦 ↔ 𝑥 ( le ‘ 𝐾 ) 𝑦 ) )
12 2 breqd ⊢ ( 𝜑 → ( 𝑦 ≤ 𝑧 ↔ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) )
13 11 12 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ↔ ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) ) )
14 2 breqd ⊢ ( 𝜑 → ( 𝑥 ≤ 𝑧 ↔ 𝑥 ( le ‘ 𝐾 ) 𝑧 ) )
15 13 14 imbi12d ⊢ ( 𝜑 → ( ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ↔ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
16 10 15 anbi12d ⊢ ( 𝜑 → ( ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ↔ ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
17 1 16 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
18 1 17 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
19 1 18 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
20 9 19 bitr4d ⊢ ( 𝜑 → ( 𝐾 ∈ Proset ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )