Metamath Proof Explorer

Theorem resspos

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

Ref Expression
Assertion resspos ( ( 𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) ∈ Poset )

Proof

Step Hyp Ref Expression
1 ovexd ⊢ ( ( 𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) ∈ V )
2 eqid ⊢ ( 𝐹 ↾s 𝐴 ) = ( 𝐹 ↾s 𝐴 )
3 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
4 2 3 ressbas ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ ( Base ‘ 𝐹 ) ) = ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) )
5 inss2 ⊢ ( 𝐴 ∩ ( Base ‘ 𝐹 ) ) ⊆ ( Base ‘ 𝐹 )
6 4 5 eqsstrrdi ⊢ ( 𝐴 ∈ 𝑉 → ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) )
7 6 adantl ⊢ ( ( 𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉 ) → ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) )
8 eqid ⊢ ( le ‘ 𝐹 ) = ( le ‘ 𝐹 )
9 3 8 ispos ⊢ ( 𝐹 ∈ Poset ↔ ( 𝐹 ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) ) )
10 9 simprbi ⊢ ( 𝐹 ∈ Poset → ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) )
11 10 adantr ⊢ ( ( 𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) )
12 ssralv ⊢ ( ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) → ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) ) )
13 12 ralimdv ⊢ ( ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) ) )
14 ssralv ⊢ ( ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) → ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) ) )
15 13 14 syld ⊢ ( ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) → ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) ) )
16 15 ralimdv ⊢ ( ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) ) )
17 ssralv ⊢ ( ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) ) )
18 16 17 syld ⊢ ( ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ⊆ ( Base ‘ 𝐹 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐹 ) ∀ 𝑦 ∈ ( Base ‘ 𝐹 ) ∀ 𝑧 ∈ ( Base ‘ 𝐹 ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) ) )
19 7 11 18 sylc ⊢ ( ( 𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) )
20 2 8 ressle ⊢ ( 𝐴 ∈ 𝑉 → ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) )
21 20 adantl ⊢ ( ( 𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉 ) → ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) )
22 breq ⊢ ( ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) → ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ↔ 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) )
23 breq ⊢ ( ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) → ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ↔ 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ) )
24 breq ⊢ ( ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) → ( 𝑦 ( le ‘ 𝐹 ) 𝑥 ↔ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) )
25 23 24 anbi12d ⊢ ( ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) → ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) ↔ ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) ) )
26 25 imbi1d ⊢ ( ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) → ( ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
27 breq ⊢ ( ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) → ( 𝑦 ( le ‘ 𝐹 ) 𝑧 ↔ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) )
28 23 27 anbi12d ⊢ ( ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) → ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) ↔ ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) ) )
29 breq ⊢ ( ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) → ( 𝑥 ( le ‘ 𝐹 ) 𝑧 ↔ 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) )
30 28 29 imbi12d ⊢ ( ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) → ( ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ↔ ( ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) ) )
31 22 26 30 3anbi123d ⊢ ( ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) → ( ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) ↔ ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) ) ) )
32 31 ralbidv ⊢ ( ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) → ( ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) ) ) )
33 32 2ralbidv ⊢ ( ( le ‘ 𝐹 ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) ) → ( ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) ) ) )
34 21 33 syl ⊢ ( ( 𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ 𝐹 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ 𝐹 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐹 ) 𝑧 ) → 𝑥 ( le ‘ 𝐹 ) 𝑧 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) ) ) )
35 19 34 mpbid ⊢ ( ( 𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉 ) → ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) ) )
36 eqid ⊢ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) = ( Base ‘ ( 𝐹 ↾s 𝐴 ) )
37 eqid ⊢ ( le ‘ ( 𝐹 ↾s 𝐴 ) ) = ( le ‘ ( 𝐹 ↾s 𝐴 ) )
38 36 37 ispos ⊢ ( ( 𝐹 ↾s 𝐴 ) ∈ Poset ↔ ( ( 𝐹 ↾s 𝐴 ) ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐹 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐹 ↾s 𝐴 ) ) 𝑧 ) ) ) )
39 1 35 38 sylanbrc ⊢ ( ( 𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉 ) → ( 𝐹 ↾s 𝐴 ) ∈ Poset )