Metamath Proof Explorer

Theorem resstos

Description: The restriction of a Toset is a Toset. (Contributed by Thierry Arnoux, 20-Jan-2018)

Ref Expression
Assertion resstos ( ( 𝐹 ∈ Toset ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) ∈ Toset )

Proof

Step Hyp Ref Expression
1 tospos ⊢ ( 𝐹 ∈ Toset → 𝐹 ∈ Poset )
2 resspos ⊢ ( ( 𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) ∈ Poset )
3 1 2 sylan ⊢ ( ( 𝐹 ∈ Toset ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) ∈ Poset )
4 eqid ⊢ ( 𝐹 ↾s 𝐴 ) = ( 𝐹 ↾s 𝐴 )
5 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
6 4 5 ressbas ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ ( Base ‘ 𝐹 ) ) = ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) )
7 inss2 ⊢ ( 𝐴 ∩ ( Base ‘ 𝐹 ) ) ⊆ ( Base ‘ 𝐹 )
8 6 7 eqsstrrdi ⊢ ( 𝐴 ∈ 𝑉 → ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) )
9 8 adantl ⊢ ( ( 𝐹 ∈ Toset ∧ 𝐴 ∈ 𝑉 ) → ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) )
10 eqid ⊢ ( le ‘ 𝐹 ) = ( le ‘ 𝐹 )
11 5 10 istos ⊢ ( 𝐹 ∈ Toset ↔ ( 𝐹 ∈ Poset ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) ) )
12 11 simprbi ⊢ ( 𝐹 ∈ Toset → ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) )
13 12 adantr ⊢ ( ( 𝐹 ∈ Toset ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) )
14 ssralv ⊢ ( ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) ) )
15 ssralv ⊢ ( ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) ) )
16 15 ralimdv ⊢ ( ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) → ( ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) ) )
17 14 16 syld ⊢ ( ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) ) )
18 9 13 17 sylc ⊢ ( ( 𝐹 ∈ Toset ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) )
19 4 10 ressle ⊢ ( 𝐴 ∈ 𝑉 → ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) )
20 19 breqd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ↔ 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ) )
21 19 breqd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑦 ( le ‘ 𝐹 ) 𝑥 ↔ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) )
22 20 21 orbi12d ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) ↔ ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∨ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) ) )
23 22 2ralbidv ⊢ ( 𝐴 ∈ 𝑉 → ( ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∨ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) ) )
24 23 adantl ⊢ ( ( 𝐹 ∈ Toset ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∨ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∨ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) ) )
25 18 24 mpbid ⊢ ( ( 𝐹 ∈ Toset ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∨ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) )
26 eqid ⊢ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) = ( Base ‘ ( 𝐹 ↾s 𝐴 ) )
27 eqid ⊢ ( le ‘ ( 𝐹 ↾s 𝐴 ) ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) )
28 26 27 istos ⊢ ( ( 𝐹 ↾s 𝐴 ) ∈ Toset ↔ ( ( 𝐹 ↾s 𝐴 ) ∈ Poset ∧ ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∨ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) ) )
29 3 25 28 sylanbrc ⊢ ( ( 𝐹 ∈ Toset ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) ∈ Toset )