Metamath Proof Explorer

Theorem dfon4

Description: Another quantifier-free definition of On . (Contributed by Scott Fenton, 4-May-2014)

Ref Expression
Assertion dfon4 ⊒On=Vβˆ–π–²π–²π–Ύπ—βˆ–IβˆͺEπ–³π—‹π–Ίπ—‡π—Œ

Proof

Step Hyp Ref Expression
1 dfon3 ⊒On=Vβˆ–ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE
2 df-ima βŠ’π–²π–²π–Ύπ—βˆ–IβˆͺEπ–³π—‹π–Ίπ—‡π—Œ=ranβ‘π–²π–²π–Ύπ—βˆ–IβˆͺEβ†Ύπ–³π—‹π–Ίπ—‡π—Œ
3 df-res βŠ’π–²π–²π–Ύπ—βˆ–IβˆͺEβ†Ύπ–³π—‹π–Ίπ—‡π—Œ=π–²π–²π–Ύπ—βˆ–IβˆͺEβˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—V
4 indif1 βŠ’π–²π–²π–Ύπ—βˆ–IβˆͺEβˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—V=π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE
5 3 4 eqtri βŠ’π–²π–²π–Ύπ—βˆ–IβˆͺEβ†Ύπ–³π—‹π–Ίπ—‡π—Œ=π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE
6 5 rneqi ⊒ranβ‘π–²π–²π–Ύπ—βˆ–IβˆͺEβ†Ύπ–³π—‹π–Ίπ—‡π—Œ=ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE
7 2 6 eqtri βŠ’π–²π–²π–Ύπ—βˆ–IβˆͺEπ–³π—‹π–Ίπ—‡π—Œ=ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE
8 7 difeq2i ⊒Vβˆ–π–²π–²π–Ύπ—βˆ–IβˆͺEπ–³π—‹π–Ίπ—‡π—Œ=Vβˆ–ranβ‘π–²π–²π–Ύπ—βˆ©π–³π—‹π–Ίπ—‡π—ŒΓ—Vβˆ–IβˆͺE
9 1 8 eqtr4i ⊒On=Vβˆ–π–²π–²π–Ύπ—βˆ–IβˆͺEπ–³π—‹π–Ίπ—‡π—Œ