Metamath Proof Explorer


Theorem trclubi

Description: The Cartesian product of the domain and range of a relation is an upper bound for its transitive closure. (Contributed by RP, 2-Jan-2020) (Revised by RP, 28-Apr-2020) (Revised by AV, 26-Mar-2021)

Ref Expression
Hypotheses trclubi.rel Rel 𝑅
trclubi.rex 𝑅 ∈ V
Assertion trclubi { 𝑠 ∣ ( 𝑅𝑠 ∧ ( 𝑠𝑠 ) ⊆ 𝑠 ) } ⊆ ( dom 𝑅 × ran 𝑅 )

Proof

Step Hyp Ref Expression
1 trclubi.rel Rel 𝑅
2 trclubi.rex 𝑅 ∈ V
3 relssdmrn ( Rel 𝑅𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) )
4 ssequn1 ( 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) ↔ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) )
5 3 4 sylib ( Rel 𝑅 → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) )
6 1 5 ax-mp ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 )
7 trclublem ( 𝑅 ∈ V → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ { 𝑠 ∣ ( 𝑅𝑠 ∧ ( 𝑠𝑠 ) ⊆ 𝑠 ) } )
8 2 7 ax-mp ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ { 𝑠 ∣ ( 𝑅𝑠 ∧ ( 𝑠𝑠 ) ⊆ 𝑠 ) }
9 6 8 eqeltrri ( dom 𝑅 × ran 𝑅 ) ∈ { 𝑠 ∣ ( 𝑅𝑠 ∧ ( 𝑠𝑠 ) ⊆ 𝑠 ) }
10 intss1 ( ( dom 𝑅 × ran 𝑅 ) ∈ { 𝑠 ∣ ( 𝑅𝑠 ∧ ( 𝑠𝑠 ) ⊆ 𝑠 ) } → { 𝑠 ∣ ( 𝑅𝑠 ∧ ( 𝑠𝑠 ) ⊆ 𝑠 ) } ⊆ ( dom 𝑅 × ran 𝑅 ) )
11 9 10 ax-mp { 𝑠 ∣ ( 𝑅𝑠 ∧ ( 𝑠𝑠 ) ⊆ 𝑠 ) } ⊆ ( dom 𝑅 × ran 𝑅 )