Metamath Proof Explorer

Theorem trclubgNEW

Description: If a relation exists then the transitive closure has an upper bound. (Contributed by RP, 24-Jul-2020)

Ref Expression
Hypothesis trclubgNEW.rex ⊢ ( 𝜑 → 𝑅 ∈ V )
Assertion trclubgNEW ( 𝜑 → ∩ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 trclubgNEW.rex ⊢ ( 𝜑 → 𝑅 ∈ V )
2 1 dmexd ⊢ ( 𝜑 → dom 𝑅 ∈ V )
3 rnexg ⊢ ( 𝑅 ∈ V → ran 𝑅 ∈ V )
4 1 3 syl ⊢ ( 𝜑 → ran 𝑅 ∈ V )
5 2 4 xpexd ⊢ ( 𝜑 → ( dom 𝑅 × ran 𝑅 ) ∈ V )
6 1 5 unexd ⊢ ( 𝜑 → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ V )
7 id ⊢ ( 𝑥 = ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) → 𝑥 = ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
8 7 7 coeq12d ⊢ ( 𝑥 = ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) → ( 𝑥 ∘ 𝑥 ) = ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) )
9 8 7 sseq12d ⊢ ( 𝑥 = ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) → ( ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ↔ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) )
10 ssun1 ⊢ 𝑅 ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) )
11 10 a1i ⊢ ( 𝜑 → 𝑅 ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
12 cnvssrndm ⊢ ◡ 𝑅 ⊆ ( ran 𝑅 × dom 𝑅 )
13 coundi ⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) = ( ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ 𝑅 ) ∪ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
14 cnvss ⊢ ( ◡ 𝑅 ⊆ ( ran 𝑅 × dom 𝑅 ) → ◡ ◡ 𝑅 ⊆ ◡ ( ran 𝑅 × dom 𝑅 ) )
15 coss2 ⊢ ( ◡ ◡ 𝑅 ⊆ ◡ ( ran 𝑅 × dom 𝑅 ) → ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ◡ ◡ 𝑅 ) ⊆ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ◡ ( ran 𝑅 × dom 𝑅 ) ) )
16 14 15 syl ⊢ ( ◡ 𝑅 ⊆ ( ran 𝑅 × dom 𝑅 ) → ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ◡ ◡ 𝑅 ) ⊆ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ◡ ( ran 𝑅 × dom 𝑅 ) ) )
17 cocnvcnv2 ⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ◡ ◡ 𝑅 ) = ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ 𝑅 )
18 cnvxp ⊢ ◡ ( ran 𝑅 × dom 𝑅 ) = ( dom 𝑅 × ran 𝑅 )
19 18 coeq2i ⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ◡ ( ran 𝑅 × dom 𝑅 ) ) = ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( dom 𝑅 × ran 𝑅 ) )
20 16 17 19 3sstr3g ⊢ ( ◡ 𝑅 ⊆ ( ran 𝑅 × dom 𝑅 ) → ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
21 ssequn1 ⊢ ( ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ 𝑅 ) ⊆ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ↔ ( ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ 𝑅 ) ∪ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ) = ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
22 20 21 sylib ⊢ ( ◡ 𝑅 ⊆ ( ran 𝑅 × dom 𝑅 ) → ( ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ 𝑅 ) ∪ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ) = ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
23 coundir ⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( dom 𝑅 × ran 𝑅 ) ) = ( ( 𝑅 ∘ ( dom 𝑅 × ran 𝑅 ) ) ∪ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
24 coss1 ⊢ ( ◡ ◡ 𝑅 ⊆ ◡ ( ran 𝑅 × dom 𝑅 ) → ( ◡ ◡ 𝑅 ∘ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( ◡ ( ran 𝑅 × dom 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
25 14 24 syl ⊢ ( ◡ 𝑅 ⊆ ( ran 𝑅 × dom 𝑅 ) → ( ◡ ◡ 𝑅 ∘ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( ◡ ( ran 𝑅 × dom 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
26 cocnvcnv1 ⊢ ( ◡ ◡ 𝑅 ∘ ( dom 𝑅 × ran 𝑅 ) ) = ( 𝑅 ∘ ( dom 𝑅 × ran 𝑅 ) )
27 18 coeq1i ⊢ ( ◡ ( ran 𝑅 × dom 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) = ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) )
28 25 26 27 3sstr3g ⊢ ( ◡ 𝑅 ⊆ ( ran 𝑅 × dom 𝑅 ) → ( 𝑅 ∘ ( 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 ⊢ ( ◡ 𝑅 ⊆ ( ran 𝑅 × dom 𝑅 ) → ( ( 𝑅 ∘ ( dom 𝑅 × ran 𝑅 ) ) ∪ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ) = ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) )
31 xptrrel ⊢ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( dom 𝑅 × ran 𝑅 )
32 ssun2 ⊢ ( dom 𝑅 × ran 𝑅 ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) )
33 31 32 sstri ⊢ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) )
34 33 a1i ⊢ ( ◡ 𝑅 ⊆ ( ran 𝑅 × dom 𝑅 ) → ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
35 30 34 eqsstrd ⊢ ( ◡ 𝑅 ⊆ ( ran 𝑅 × dom 𝑅 ) → ( ( 𝑅 ∘ ( dom 𝑅 × ran 𝑅 ) ) ∪ ( ( dom 𝑅 × ran 𝑅 ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
36 23 35 eqsstrid ⊢ ( ◡ 𝑅 ⊆ ( ran 𝑅 × dom 𝑅 ) → ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
37 22 36 eqsstrd ⊢ ( ◡ 𝑅 ⊆ ( ran 𝑅 × dom 𝑅 ) → ( ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ 𝑅 ) ∪ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
38 13 37 eqsstrid ⊢ ( ◡ 𝑅 ⊆ ( ran 𝑅 × dom 𝑅 ) → ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
39 12 38 mp1i ⊢ ( 𝜑 → ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∘ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
40 6 9 11 39 clublem ⊢ ( 𝜑 → ∩ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )