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 ∧ ∀ 𝑥𝐵𝑦𝐵𝑧𝐵 ( 𝑥 𝑥 ∧ ( ( 𝑥 𝑦𝑦 𝑧 ) → 𝑥 𝑧 ) ) ) )