Step |
Hyp |
Ref |
Expression |
1 |
|
trclubi.rel |
⊢ Rel 𝑅 |
2 |
|
trclubi.rex |
⊢ 𝑅 ∈ V |
3 |
|
relssdmrn |
⊢ ( Rel 𝑅 → 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) ) |
4 |
|
ssequn1 |
⊢ ( 𝑅 ⊆ ( dom 𝑅 × ran 𝑅 ) ↔ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) ) |
5 |
3 4
|
sylib |
⊢ ( Rel 𝑅 → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) ) |
6 |
1 5
|
ax-mp |
⊢ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) = ( dom 𝑅 × ran 𝑅 ) |
7 |
|
trclublem |
⊢ ( 𝑅 ∈ V → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ { 𝑠 ∣ ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ) |
8 |
2 7
|
ax-mp |
⊢ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ { 𝑠 ∣ ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } |
9 |
6 8
|
eqeltrri |
⊢ ( dom 𝑅 × ran 𝑅 ) ∈ { 𝑠 ∣ ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } |
10 |
|
intss1 |
⊢ ( ( dom 𝑅 × ran 𝑅 ) ∈ { 𝑠 ∣ ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } → ∩ { 𝑠 ∣ ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ⊆ ( dom 𝑅 × ran 𝑅 ) ) |
11 |
9 10
|
ax-mp |
⊢ ∩ { 𝑠 ∣ ( 𝑅 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) } ⊆ ( dom 𝑅 × ran 𝑅 ) |