Description: Obsolete version of jech9.3 as of 29-Sep-2026. (Contributed by NM, 4-Oct-2003) (Revised by Mario Carneiro, 8-Jun-2013) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | jech9.3OLD | |- U_ x e. On ( R1 ` x ) = _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | r1fnon | |- R1 Fn On |
|
| 2 | fniunfv | |- ( R1 Fn On -> U_ x e. On ( R1 ` x ) = U. ran R1 ) |
|
| 3 | 1 2 | ax-mp | |- U_ x e. On ( R1 ` x ) = U. ran R1 |
| 4 | fndm | |- ( R1 Fn On -> dom R1 = On ) |
|
| 5 | 1 4 | ax-mp | |- dom R1 = On |
| 6 | 5 | imaeq2i | |- ( R1 " dom R1 ) = ( R1 " On ) |
| 7 | imadmrn | |- ( R1 " dom R1 ) = ran R1 |
|
| 8 | 6 7 | eqtr3i | |- ( R1 " On ) = ran R1 |
| 9 | 8 | unieqi | |- U. ( R1 " On ) = U. ran R1 |
| 10 | unir1 | |- U. ( R1 " On ) = _V |
|
| 11 | 3 9 10 | 3eqtr2i | |- U_ x e. On ( R1 ` x ) = _V |