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