Step |
Hyp |
Ref |
Expression |
1 |
|
elex |
⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V ) |
2 |
|
trclexlem |
⊢ ( 𝑅 ∈ V → ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ∈ V ) |
3 |
|
trclubg |
⊢ ( 𝑅 ∈ V → ∩ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ⊆ ( 𝑅 ∪ ( dom 𝑅 × ran 𝑅 ) ) ) |
4 |
2 3
|
ssexd |
⊢ ( 𝑅 ∈ V → ∩ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ∈ V ) |
5 |
|
trcleq1 |
⊢ ( 𝑟 = 𝑅 → ∩ { 𝑥 ∣ ( 𝑟 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } = ∩ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ) |
6 |
|
df-trcl |
⊢ t+ = ( 𝑟 ∈ V ↦ ∩ { 𝑥 ∣ ( 𝑟 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ) |
7 |
5 6
|
fvmptg |
⊢ ( ( 𝑅 ∈ V ∧ ∩ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ∈ V ) → ( t+ ‘ 𝑅 ) = ∩ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ) |
8 |
1 4 7
|
syl2anc2 |
⊢ ( 𝑅 ∈ 𝑉 → ( t+ ‘ 𝑅 ) = ∩ { 𝑥 ∣ ( 𝑅 ⊆ 𝑥 ∧ ( 𝑥 ∘ 𝑥 ) ⊆ 𝑥 ) } ) |