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 )