Theorem trclubgi

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

	Ref	Expression
Hypothesis	trclubgi.rex	⊢ 𝑅 ∈ V
Assertion	trclubgi	⊢ ∩ { 𝑠 ∣ ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		trclubgi.rex	⊢ 𝑅 ∈ V
2		trclublem	⊢ ( 𝑅 ∈ V → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ { 𝑠 ∣ ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } )
3		intss1	⊢ ( ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ { 𝑠 ∣ ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } → ∩ { 𝑠 ∣ ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) )
4	1 2 3	mp2b	⊢ ∩ { 𝑠 ∣ ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) )