Description: Obsolete version of rnin as of 10-Jun-2026. (Contributed by NM, 15-Sep-2004) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rninOLD | |- ran ( A i^i B ) C_ ( ran A i^i ran B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cnvin | |- `' ( A i^i B ) = ( `' A i^i `' B ) |
|
| 2 | 1 | dmeqi | |- dom `' ( A i^i B ) = dom ( `' A i^i `' B ) |
| 3 | dmin | |- dom ( `' A i^i `' B ) C_ ( dom `' A i^i dom `' B ) |
|
| 4 | 2 3 | eqsstri | |- dom `' ( A i^i B ) C_ ( dom `' A i^i dom `' B ) |
| 5 | df-rn | |- ran ( A i^i B ) = dom `' ( A i^i B ) |
|
| 6 | df-rn | |- ran A = dom `' A |
|
| 7 | df-rn | |- ran B = dom `' B |
|
| 8 | 6 7 | ineq12i | |- ( ran A i^i ran B ) = ( dom `' A i^i dom `' B ) |
| 9 | 4 5 8 | 3sstr4i | |- ran ( A i^i B ) C_ ( ran A i^i ran B ) |