Theorem trclubNEW

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

	Ref	Expression
Hypotheses	trclubNEW.rex	⊢ ( 𝜑 → 𝑅 ∈ V )
	trclubNEW.rel	⊢ ( 𝜑 → Rel 𝑅 )
Assertion	trclubNEW	⊢ ( 𝜑 → ∩ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ⊆ ( dom 𝑅 × ran 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		trclubNEW.rex	⊢ ( 𝜑 → 𝑅 ∈ V )
2		trclubNEW.rel	⊢ ( 𝜑 → Rel 𝑅 )
3	1	trclubgNEW	⊢ ( 𝜑 → ∩ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
4		relssdmrn	⊢ ( Rel 𝑅 → 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) )
5	2 4	syl	⊢ ( 𝜑 → 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) )
6		ssequn1	⊢ ( 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) ↔ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) )
7	5 6	sylib	⊢ ( 𝜑 → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) )
8	3 7	sseqtrd	⊢ ( 𝜑 → ∩ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ⊆ ( dom 𝑅 × ran 𝑅 ) )