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 𝑅 )