Metamath Proof Explorer

Theorem isprs

Description: Property of being a preordered set. (Contributed by Stefan O'Rear, 31-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 isprs.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 isprs.l ⊢ ≤ = ( le ‘ 𝐾 )
3 fveq2 ⊢ ( 𝑓 = 𝐾 → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐾 ) )
4 fveq2 ⊢ ( 𝑓 = 𝐾 → ( le ‘ 𝑓 ) = ( le ‘ 𝐾 ) )
5 4 sbceq1d ⊢ ( 𝑓 = 𝐾 → ( [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ [ ( le ‘ 𝐾 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) )
6 3 5 sbceqbid ⊢ ( 𝑓 = 𝐾 → ( [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ [ ( Base ‘ 𝐾 ) / 𝑏 ] [ ( le ‘ 𝐾 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) )
7 fvex ⊢ ( Base ‘ 𝐾 ) ∈ V
8 fvex ⊢ ( le ‘ 𝐾 ) ∈ V
9 eqtr3 ⊢ ( ( 𝑏 = ( Base ‘ 𝐾 ) ∧ 𝐵 = ( Base ‘ 𝐾 ) ) → 𝑏 = 𝐵 )
10 1 9 mpan2 ⊢ ( 𝑏 = ( Base ‘ 𝐾 ) → 𝑏 = 𝐵 )
11 raleq ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) )
12 11 raleqbi1dv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) )
13 12 raleqbi1dv ⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) )
14 10 13 syl ⊢ ( 𝑏 = ( Base ‘ 𝐾 ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ) )
15 eqtr3 ⊢ ( ( 𝑟 = ( le ‘ 𝐾 ) ∧ ≤ = ( le ‘ 𝐾 ) ) → 𝑟 = ≤ )
16 2 15 mpan2 ⊢ ( 𝑟 = ( le ‘ 𝐾 ) → 𝑟 = ≤ )
17 breq ⊢ ( 𝑟 = ≤ → ( 𝑥 𝑟 𝑥 ↔ 𝑥 ≤ 𝑥 ) )
18 breq ⊢ ( 𝑟 = ≤ → ( 𝑥 𝑟 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
19 breq ⊢ ( 𝑟 = ≤ → ( 𝑦 𝑟 𝑧 ↔ 𝑦 ≤ 𝑧 ) )
20 18 19 anbi12d ⊢ ( 𝑟 = ≤ → ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) ↔ ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ) )
21 breq ⊢ ( 𝑟 = ≤ → ( 𝑥 𝑟 𝑧 ↔ 𝑥 ≤ 𝑧 ) )
22 20 21 imbi12d ⊢ ( 𝑟 = ≤ → ( ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ↔ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) )
23 17 22 anbi12d ⊢ ( 𝑟 = ≤ → ( ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )
24 23 ralbidv ⊢ ( 𝑟 = ≤ → ( ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )
25 24 2ralbidv ⊢ ( 𝑟 = ≤ → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )
26 16 25 syl ⊢ ( 𝑟 = ( le ‘ 𝐾 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )
27 14 26 sylan9bb ⊢ ( ( 𝑏 = ( Base ‘ 𝐾 ) ∧ 𝑟 = ( le ‘ 𝐾 ) ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )
28 7 8 27 sbc2ie ⊢ ( [ ( Base ‘ 𝐾 ) / 𝑏 ] [ ( le ‘ 𝐾 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) )
29 6 28 bitrdi ⊢ ( 𝑓 = 𝐾 → ( [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )
30 df-proset ⊢ Proset = { 𝑓 ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑥 ∧ ( ( 𝑥 𝑟 𝑦 ∧ 𝑦 𝑟 𝑧 ) → 𝑥 𝑟 𝑧 ) ) }
31 29 30 elab4g ⊢ ( 𝐾 ∈ Proset ↔ ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )