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

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 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) )