Metamath Proof Explorer


Definition df-trs

Description: Define the class of all transitive sets (versus the transitive class defined in df-tr ). It is used only by df-trrels .

Note the similarity of the definitions of df-refs , df-syms and df-trs . (Contributed by Peter Mazsa, 17-Jul-2021)

Ref Expression
Assertion df-trs Trs = { 𝑥 ∣ ( ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ∘ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctrs Trs
1 vx 𝑥
2 1 cv 𝑥
3 2 cdm dom 𝑥
4 2 crn ran 𝑥
5 3 4 cxp ( dom 𝑥 × ran 𝑥 )
6 2 5 cin ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) )
7 6 6 ccom ( ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ∘ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) )
8 cssr S
9 7 6 8 wbr ( ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ∘ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) )
10 9 1 cab { 𝑥 ∣ ( ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ∘ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) }
11 0 10 wceq Trs = { 𝑥 ∣ ( ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ∘ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) }