Step |
Hyp |
Ref |
Expression |
1 |
|
df-rn |
⊢ ran 𝐵 = dom ◡ 𝐵 |
2 |
1
|
eleq2i |
⊢ ( 𝐴 ∈ ran 𝐵 ↔ 𝐴 ∈ dom ◡ 𝐵 ) |
3 |
|
eldm3 |
⊢ ( 𝐴 ∈ dom ◡ 𝐵 ↔ ( ◡ 𝐵 ↾ { 𝐴 } ) ≠ ∅ ) |
4 |
|
cnvxp |
⊢ ◡ ( V × { 𝐴 } ) = ( { 𝐴 } × V ) |
5 |
4
|
ineq2i |
⊢ ( ◡ 𝐵 ∩ ◡ ( V × { 𝐴 } ) ) = ( ◡ 𝐵 ∩ ( { 𝐴 } × V ) ) |
6 |
|
cnvin |
⊢ ◡ ( 𝐵 ∩ ( V × { 𝐴 } ) ) = ( ◡ 𝐵 ∩ ◡ ( V × { 𝐴 } ) ) |
7 |
|
df-res |
⊢ ( ◡ 𝐵 ↾ { 𝐴 } ) = ( ◡ 𝐵 ∩ ( { 𝐴 } × V ) ) |
8 |
5 6 7
|
3eqtr4ri |
⊢ ( ◡ 𝐵 ↾ { 𝐴 } ) = ◡ ( 𝐵 ∩ ( V × { 𝐴 } ) ) |
9 |
8
|
eqeq1i |
⊢ ( ( ◡ 𝐵 ↾ { 𝐴 } ) = ∅ ↔ ◡ ( 𝐵 ∩ ( V × { 𝐴 } ) ) = ∅ ) |
10 |
|
relinxp |
⊢ Rel ( 𝐵 ∩ ( V × { 𝐴 } ) ) |
11 |
|
cnveq0 |
⊢ ( Rel ( 𝐵 ∩ ( V × { 𝐴 } ) ) → ( ( 𝐵 ∩ ( V × { 𝐴 } ) ) = ∅ ↔ ◡ ( 𝐵 ∩ ( V × { 𝐴 } ) ) = ∅ ) ) |
12 |
10 11
|
ax-mp |
⊢ ( ( 𝐵 ∩ ( V × { 𝐴 } ) ) = ∅ ↔ ◡ ( 𝐵 ∩ ( V × { 𝐴 } ) ) = ∅ ) |
13 |
9 12
|
bitr4i |
⊢ ( ( ◡ 𝐵 ↾ { 𝐴 } ) = ∅ ↔ ( 𝐵 ∩ ( V × { 𝐴 } ) ) = ∅ ) |
14 |
13
|
necon3bii |
⊢ ( ( ◡ 𝐵 ↾ { 𝐴 } ) ≠ ∅ ↔ ( 𝐵 ∩ ( V × { 𝐴 } ) ) ≠ ∅ ) |
15 |
2 3 14
|
3bitri |
⊢ ( 𝐴 ∈ ran 𝐵 ↔ ( 𝐵 ∩ ( V × { 𝐴 } ) ) ≠ ∅ ) |