Metamath Proof Explorer


Theorem psss

Description: Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010)

Ref Expression
Assertion psss ( 𝑅 ∈ PosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel )

Proof

Step Hyp Ref Expression
1 inss1 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑅
2 psrel ( 𝑅 ∈ PosetRel → Rel 𝑅 )
3 relss ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ 𝑅 → ( Rel 𝑅 → Rel ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
4 1 2 3 mpsyl ( 𝑅 ∈ PosetRel → Rel ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )
5 pstr2 ( 𝑅 ∈ PosetRel → ( 𝑅𝑅 ) ⊆ 𝑅 )
6 trinxp ( ( 𝑅𝑅 ) ⊆ 𝑅 → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )
7 5 6 syl ( 𝑅 ∈ PosetRel → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )
8 uniin ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ( 𝐴 × 𝐴 ) )
9 8 unissi ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ( 𝐴 × 𝐴 ) )
10 uniin ( 𝑅 ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ( 𝐴 × 𝐴 ) )
11 9 10 sstri ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ( 𝐴 × 𝐴 ) )
12 elin ( 𝑥 ∈ ( 𝑅 ( 𝐴 × 𝐴 ) ) ↔ ( 𝑥 𝑅𝑥 ( 𝐴 × 𝐴 ) ) )
13 unixpid ( 𝐴 × 𝐴 ) = 𝐴
14 13 eleq2i ( 𝑥 ( 𝐴 × 𝐴 ) ↔ 𝑥𝐴 )
15 simprr ( ( 𝑅 ∈ PosetRel ∧ ( 𝑥 𝑅𝑥𝐴 ) ) → 𝑥𝐴 )
16 psdmrn ( 𝑅 ∈ PosetRel → ( dom 𝑅 = 𝑅 ∧ ran 𝑅 = 𝑅 ) )
17 16 simpld ( 𝑅 ∈ PosetRel → dom 𝑅 = 𝑅 )
18 17 eleq2d ( 𝑅 ∈ PosetRel → ( 𝑥 ∈ dom 𝑅𝑥 𝑅 ) )
19 18 biimpar ( ( 𝑅 ∈ PosetRel ∧ 𝑥 𝑅 ) → 𝑥 ∈ dom 𝑅 )
20 eqid dom 𝑅 = dom 𝑅
21 20 psref ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → 𝑥 𝑅 𝑥 )
22 19 21 syldan ( ( 𝑅 ∈ PosetRel ∧ 𝑥 𝑅 ) → 𝑥 𝑅 𝑥 )
23 22 adantrr ( ( 𝑅 ∈ PosetRel ∧ ( 𝑥 𝑅𝑥𝐴 ) ) → 𝑥 𝑅 𝑥 )
24 brinxp2 ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ↔ ( ( 𝑥𝐴𝑥𝐴 ) ∧ 𝑥 𝑅 𝑥 ) )
25 15 15 23 24 syl21anbrc ( ( 𝑅 ∈ PosetRel ∧ ( 𝑥 𝑅𝑥𝐴 ) ) → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 )
26 25 expr ( ( 𝑅 ∈ PosetRel ∧ 𝑥 𝑅 ) → ( 𝑥𝐴𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
27 14 26 syl5bi ( ( 𝑅 ∈ PosetRel ∧ 𝑥 𝑅 ) → ( 𝑥 ( 𝐴 × 𝐴 ) → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
28 27 expimpd ( 𝑅 ∈ PosetRel → ( ( 𝑥 𝑅𝑥 ( 𝐴 × 𝐴 ) ) → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
29 12 28 syl5bi ( 𝑅 ∈ PosetRel → ( 𝑥 ∈ ( 𝑅 ( 𝐴 × 𝐴 ) ) → 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
30 29 ralrimiv ( 𝑅 ∈ PosetRel → ∀ 𝑥 ∈ ( 𝑅 ( 𝐴 × 𝐴 ) ) 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 )
31 ssralv ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ⊆ ( 𝑅 ( 𝐴 × 𝐴 ) ) → ( ∀ 𝑥 ∈ ( 𝑅 ( 𝐴 × 𝐴 ) ) 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 → ∀ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) )
32 11 30 31 mpsyl ( 𝑅 ∈ PosetRel → ∀ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 )
33 1 ssbri ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦𝑥 𝑅 𝑦 )
34 1 ssbri ( 𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥𝑦 𝑅 𝑥 )
35 psasym ( ( 𝑅 ∈ PosetRel ∧ 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 )
36 35 3expib ( 𝑅 ∈ PosetRel → ( ( 𝑥 𝑅 𝑦𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 ) )
37 33 34 36 syl2ani ( 𝑅 ∈ PosetRel → ( ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) → 𝑥 = 𝑦 ) )
38 37 alrimivv ( 𝑅 ∈ PosetRel → ∀ 𝑥𝑦 ( ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) → 𝑥 = 𝑦 ) )
39 asymref2 ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∩ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( I ↾ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( ∀ 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ∧ ∀ 𝑥𝑦 ( ( 𝑥 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑦𝑦 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
40 32 38 39 sylanbrc ( 𝑅 ∈ PosetRel → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∩ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( I ↾ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
41 inex1g ( 𝑅 ∈ PosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
42 isps ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel ↔ ( Rel ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∩ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( I ↾ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) )
43 41 42 syl ( 𝑅 ∈ PosetRel → ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel ↔ ( Rel ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∧ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∩ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( I ↾ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) ) )
44 4 7 40 43 mpbir3and ( 𝑅 ∈ PosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel )