Metamath Proof Explorer

Theorem rntrclfvOAI

Description: The range of the transitive closure is equal to the range of the relation. (Contributed by OpenAI, 7-Jul-2020)

Ref Expression
Assertion rntrclfvOAI ⊢ R ∈ V → ran ⁡ t+ ⁡ R = ran ⁡ R

Proof

Step Hyp Ref Expression
1 trclfvub ⊢ R ∈ V → t+ ⁡ R ⊆ R ∪ dom ⁡ R × ran ⁡ R
2 rnss ⊢ t+ ⁡ R ⊆ R ∪ dom ⁡ R × ran ⁡ R → ran ⁡ t+ ⁡ R ⊆ ran ⁡ R ∪ dom ⁡ R × ran ⁡ R
3 1 2 syl ⊢ R ∈ V → ran ⁡ t+ ⁡ R ⊆ ran ⁡ R ∪ dom ⁡ R × ran ⁡ R
4 rnun ⊢ ran ⁡ R ∪ dom ⁡ R × ran ⁡ R = ran ⁡ R ∪ ran ⁡ dom ⁡ R × ran ⁡ R
5 4 a1i ⊢ R ∈ V → ran ⁡ R ∪ dom ⁡ R × ran ⁡ R = ran ⁡ R ∪ ran ⁡ dom ⁡ R × ran ⁡ R
6 rnxpss ⊢ ran ⁡ dom ⁡ R × ran ⁡ R ⊆ ran ⁡ R
7 ssequn2 ⊢ ran ⁡ dom ⁡ R × ran ⁡ R ⊆ ran ⁡ R ↔ ran ⁡ R ∪ ran ⁡ dom ⁡ R × ran ⁡ R = ran ⁡ R
8 6 7 mpbi ⊢ ran ⁡ R ∪ ran ⁡ dom ⁡ R × ran ⁡ R = ran ⁡ R
9 5 8 syl6eq ⊢ R ∈ V → ran ⁡ R ∪ dom ⁡ R × ran ⁡ R = ran ⁡ R
10 3 9 sseqtrd ⊢ R ∈ V → ran ⁡ t+ ⁡ R ⊆ ran ⁡ R
11 trclfvlb ⊢ R ∈ V → R ⊆ t+ ⁡ R
12 rnss ⊢ R ⊆ t+ ⁡ R → ran ⁡ R ⊆ ran ⁡ t+ ⁡ R
13 11 12 syl ⊢ R ∈ V → ran ⁡ R ⊆ ran ⁡ t+ ⁡ R
14 10 13 eqssd ⊢ R ∈ V → ran ⁡ t+ ⁡ R = ran ⁡ R