Metamath Proof Explorer

Theorem trrelsuperrel2dg

Description: Concrete construction of a superclass of relation R which is a transitive relation. (Contributed by RP, 20-Jul-2020)

Ref Expression
Hypothesis trrelsuperrel2dg.s ⊢ ( 𝜑 → 𝑆 = ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
Assertion trrelsuperrel2dg ( 𝜑 → ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 trrelsuperrel2dg.s ⊢ ( 𝜑 → 𝑆 = ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
2 ssun1 ⊢ 𝑅 ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) )
3 2 1 sseqtrrid ⊢ ( 𝜑 → 𝑅 ⊆ 𝑆 )
4 xptrrel ⊢ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( dom 𝑅 × ran 𝑅 )
5 ssun2 ⊢ ( dom 𝑅 × ran 𝑅 ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) )
6 4 5 sstri ⊢ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) )
7 6 a1i ⊢ ( 𝜑 → ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
8 1 1 coeq12d ⊢ ( 𝜑 → ( 𝑆 ∘ 𝑆 ) = ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) )
9 coundir ⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) = ( ( 𝑅 ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ∪ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) )
10 relcnv ⊢ Rel ◡ ◡ 𝑅
11 cocnvcnv1 ⊢ ( ◡ ◡ 𝑅 ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) = ( 𝑅 ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
12 relssdmrn ⊢ ( Rel ◡ ◡ 𝑅 → ◡ ◡ 𝑅 ⊆ ( dom ◡ ◡ 𝑅 × ran ◡ ◡ 𝑅 ) )
13 dmcnvcnv ⊢ dom ◡ ◡ 𝑅 = dom 𝑅
14 rncnvcnv ⊢ ran ◡ ◡ 𝑅 = ran 𝑅
15 13 14 xpeq12i ⊢ ( dom ◡ ◡ 𝑅 × ran ◡ ◡ 𝑅 ) = ( dom 𝑅 × ran 𝑅 )
16 12 15 sseqtrdi ⊢ ( Rel ◡ ◡ 𝑅 → ◡ ◡ 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) )
17 coss1 ⊢ ( ◡ ◡ 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) → ( ◡ ◡ 𝑅 ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) )
18 16 17 syl ⊢ ( Rel ◡ ◡ 𝑅 → ( ◡ ◡ 𝑅 ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) )
19 11 18 eqsstrrid ⊢ ( Rel ◡ ◡ 𝑅 → ( 𝑅 ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) )
20 ssequn1 ⊢ ( ( 𝑅 ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ↔ ( ( 𝑅 ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ∪ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ) = ( ( dom 𝑅 × ran 𝑅 ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) )
21 19 20 sylib ⊢ ( Rel ◡ ◡ 𝑅 → ( ( 𝑅 ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ∪ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ) = ( ( dom 𝑅 × ran 𝑅 ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) )
22 10 21 ax-mp ⊢ ( ( 𝑅 ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ∪ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ) = ( ( dom 𝑅 × ran 𝑅 ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
23 9 22 eqtri ⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) = ( ( dom 𝑅 × ran 𝑅 ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
24 coundi ⊢ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) = ( ( ( dom 𝑅 × ran 𝑅 ) ∘ 𝑅 ) ∪ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
25 cocnvcnv2 ⊢ ( ( dom 𝑅 × ran 𝑅 ) ∘ ◡ ◡ 𝑅 ) = ( ( dom 𝑅 × ran 𝑅 ) ∘ 𝑅 )
26 coss2 ⊢ ( ◡ ◡ 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) → ( ( dom 𝑅 × ran 𝑅 ) ∘ ◡ ◡ 𝑅 ) ⊆ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
27 16 26 syl ⊢ ( Rel ◡ ◡ 𝑅 → ( ( dom 𝑅 × ran 𝑅 ) ∘ ◡ ◡ 𝑅 ) ⊆ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
28 25 27 eqsstrrid ⊢ ( Rel ◡ ◡ 𝑅 → ( ( dom 𝑅 × ran 𝑅 ) ∘ 𝑅 ) ⊆ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
29 ssequn1 ⊢ ( ( ( dom 𝑅 × ran 𝑅 ) ∘ 𝑅 ) ⊆ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ↔ ( ( ( dom 𝑅 × ran 𝑅 ) ∘ 𝑅 ) ∪ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ) = ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
30 28 29 sylib ⊢ ( Rel ◡ ◡ 𝑅 → ( ( ( dom 𝑅 × ran 𝑅 ) ∘ 𝑅 ) ∪ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ) = ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
31 10 30 ax-mp ⊢ ( ( ( dom 𝑅 × ran 𝑅 ) ∘ 𝑅 ) ∪ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ) = ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) )
32 24 31 eqtri ⊢ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) = ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) )
33 23 32 eqtri ⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) = ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) )
34 8 33 eqtrdi ⊢ ( 𝜑 → ( 𝑆 ∘ 𝑆 ) = ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
35 7 34 1 3sstr4d ⊢ ( 𝜑 → ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 )
36 3 35 jca ⊢ ( 𝜑 → ( 𝑅 ⊆ 𝑆 ∧ ( 𝑆 ∘ 𝑆 ) ⊆ 𝑆 ) )