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 𝑥 ) ) } |
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 𝑥 ) ) } |