Theorem trclub

Description: The Cartesian product of the domain and range of a relation is an upper bound for its transitive closure. (Contributed by RP, 17-May-2020)

	Ref	Expression
Assertion	trclub	⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ⊆ ( dom 𝑅 × ran 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		relssdmrn	⊢ ( Rel 𝑅 → 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) )
2		ssequn1	⊢ ( 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) ↔ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) )
3	1 2	sylib	⊢ ( Rel 𝑅 → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) )
4		trclublem	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } )
5		eleq1	⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) → ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ↔ ( dom 𝑅 × ran 𝑅 ) ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ) )
6	5	biimpa	⊢ ( ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) ∧ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ) → ( dom 𝑅 × ran 𝑅 ) ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } )
7	3 4 6	syl2anr	⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ( dom 𝑅 × ran 𝑅 ) ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } )
8		intss1	⊢ ( ( dom 𝑅 × ran 𝑅 ) ∈ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } → ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ⊆ ( dom 𝑅 × ran 𝑅 ) )
9	7 8	syl	⊢ ( ( 𝑅 ∈ 𝑉 ∧ Rel 𝑅 ) → ∩ { 𝑟 ∣ ( 𝑅 ⊆ 𝑟 ∧ ( 𝑟 ∘ 𝑟 ) ⊆ 𝑟 ) } ⊆ ( dom 𝑅 × ran 𝑅 ) )