Metamath Proof Explorer


Theorem istos

Description: The predicate "is a toset". (Contributed by FL, 17-Nov-2014)

Ref Expression
Hypotheses istos.b 𝐵 = ( Base ‘ 𝐾 )
istos.l = ( le ‘ 𝐾 )
Assertion istos ( 𝐾 ∈ Toset ↔ ( 𝐾 ∈ Poset ∧ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 istos.b 𝐵 = ( Base ‘ 𝐾 )
2 istos.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 eqtr ( ( 𝑏 = ( Base ‘ 𝐾 ) ∧ ( Base ‘ 𝐾 ) = 𝐵 ) → 𝑏 = 𝐵 )
10 eqtr ( ( 𝑟 = ( le ‘ 𝐾 ) ∧ ( le ‘ 𝐾 ) = ) → 𝑟 = )
11 breq ( 𝑟 = → ( 𝑥 𝑟 𝑦𝑥 𝑦 ) )
12 breq ( 𝑟 = → ( 𝑦 𝑟 𝑥𝑦 𝑥 ) )
13 11 12 orbi12d ( 𝑟 = → ( ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ( 𝑥 𝑦𝑦 𝑥 ) ) )
14 13 2ralbidv ( 𝑟 = → ( ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 𝑦𝑦 𝑥 ) ) )
15 raleq ( 𝑏 = 𝐵 → ( ∀ 𝑦𝑏 ( 𝑥 𝑦𝑦 𝑥 ) ↔ ∀ 𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) )
16 15 raleqbi1dv ( 𝑏 = 𝐵 → ( ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 𝑦𝑦 𝑥 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) )
17 14 16 sylan9bb ( ( 𝑟 = 𝑏 = 𝐵 ) → ( ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) )
18 17 ex ( 𝑟 = → ( 𝑏 = 𝐵 → ( ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) ) )
19 10 18 syl ( ( 𝑟 = ( le ‘ 𝐾 ) ∧ ( le ‘ 𝐾 ) = ) → ( 𝑏 = 𝐵 → ( ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) ) )
20 19 expcom ( ( le ‘ 𝐾 ) = → ( 𝑟 = ( le ‘ 𝐾 ) → ( 𝑏 = 𝐵 → ( ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) ) ) )
21 20 eqcoms ( = ( le ‘ 𝐾 ) → ( 𝑟 = ( le ‘ 𝐾 ) → ( 𝑏 = 𝐵 → ( ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) ) ) )
22 2 21 ax-mp ( 𝑟 = ( le ‘ 𝐾 ) → ( 𝑏 = 𝐵 → ( ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) ) )
23 9 22 syl5com ( ( 𝑏 = ( Base ‘ 𝐾 ) ∧ ( Base ‘ 𝐾 ) = 𝐵 ) → ( 𝑟 = ( le ‘ 𝐾 ) → ( ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) ) )
24 23 expcom ( ( Base ‘ 𝐾 ) = 𝐵 → ( 𝑏 = ( Base ‘ 𝐾 ) → ( 𝑟 = ( le ‘ 𝐾 ) → ( ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) ) ) )
25 24 eqcoms ( 𝐵 = ( Base ‘ 𝐾 ) → ( 𝑏 = ( Base ‘ 𝐾 ) → ( 𝑟 = ( le ‘ 𝐾 ) → ( ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) ) ) )
26 1 25 ax-mp ( 𝑏 = ( Base ‘ 𝐾 ) → ( 𝑟 = ( le ‘ 𝐾 ) → ( ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) ) )
27 26 imp ( ( 𝑏 = ( Base ‘ 𝐾 ) ∧ 𝑟 = ( le ‘ 𝐾 ) ) → ( ∀ 𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) )
28 7 8 27 sbc2ie ( [ ( Base ‘ 𝐾 ) / 𝑏 ] [ ( le ‘ 𝐾 ) / 𝑟 ]𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) )
29 6 28 bitrdi ( 𝑓 = 𝐾 → ( [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ]𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) )
30 df-toset Toset = { 𝑓 ∈ Poset ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ]𝑥𝑏𝑦𝑏 ( 𝑥 𝑟 𝑦𝑦 𝑟 𝑥 ) }
31 29 30 elrab2 ( 𝐾 ∈ Toset ↔ ( 𝐾 ∈ Poset ∧ ∀ 𝑥𝐵𝑦𝐵 ( 𝑥 𝑦𝑦 𝑥 ) ) )