Theorem dfon4

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

	Ref	Expression
Assertion	dfon4	$$⊢\mathrm{On}=\mathrm{V}\setminus \left(\mathrm{𝖲𝖲𝖾𝗍}\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)\left[\mathrm{𝖳𝗋𝖺𝗇𝗌}\right]$$

Proof

Step	Hyp	Ref	Expression
1		dfon3	$$⊢\mathrm{On}=\mathrm{V}\setminus \mathrm{ran}\left(\left(\mathrm{𝖲𝖲𝖾𝗍}\cap \left(\mathrm{𝖳𝗋𝖺𝗇𝗌}\times \mathrm{V}\right)\right)\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)$$
2		df-ima	$$⊢\left(\mathrm{𝖲𝖲𝖾𝗍}\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)\left[\mathrm{𝖳𝗋𝖺𝗇𝗌}\right]=\mathrm{ran}\left({\left(\mathrm{𝖲𝖲𝖾𝗍}\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)\upharpoonright }_{\mathrm{𝖳𝗋𝖺𝗇𝗌}}\right)$$
3		df-res	$$⊢{\left(\mathrm{𝖲𝖲𝖾𝗍}\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)\upharpoonright }_{\mathrm{𝖳𝗋𝖺𝗇𝗌}}=\left(\mathrm{𝖲𝖲𝖾𝗍}\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)\cap \left(\mathrm{𝖳𝗋𝖺𝗇𝗌}\times \mathrm{V}\right)$$
4		indif1	$$⊢\left(\mathrm{𝖲𝖲𝖾𝗍}\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)\cap \left(\mathrm{𝖳𝗋𝖺𝗇𝗌}\times \mathrm{V}\right)=\left(\mathrm{𝖲𝖲𝖾𝗍}\cap \left(\mathrm{𝖳𝗋𝖺𝗇𝗌}\times \mathrm{V}\right)\right)\setminus \left(\mathrm{I}\cup \mathrm{E}\right)$$
5	3 4	eqtri	$$⊢{\left(\mathrm{𝖲𝖲𝖾𝗍}\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)\upharpoonright }_{\mathrm{𝖳𝗋𝖺𝗇𝗌}}=\left(\mathrm{𝖲𝖲𝖾𝗍}\cap \left(\mathrm{𝖳𝗋𝖺𝗇𝗌}\times \mathrm{V}\right)\right)\setminus \left(\mathrm{I}\cup \mathrm{E}\right)$$
6	5	rneqi	$$⊢\mathrm{ran}\left({\left(\mathrm{𝖲𝖲𝖾𝗍}\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)\upharpoonright }_{\mathrm{𝖳𝗋𝖺𝗇𝗌}}\right)=\mathrm{ran}\left(\left(\mathrm{𝖲𝖲𝖾𝗍}\cap \left(\mathrm{𝖳𝗋𝖺𝗇𝗌}\times \mathrm{V}\right)\right)\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)$$
7	2 6	eqtri	$$⊢\left(\mathrm{𝖲𝖲𝖾𝗍}\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)\left[\mathrm{𝖳𝗋𝖺𝗇𝗌}\right]=\mathrm{ran}\left(\left(\mathrm{𝖲𝖲𝖾𝗍}\cap \left(\mathrm{𝖳𝗋𝖺𝗇𝗌}\times \mathrm{V}\right)\right)\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)$$
8	7	difeq2i	$$⊢\mathrm{V}\setminus \left(\mathrm{𝖲𝖲𝖾𝗍}\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)\left[\mathrm{𝖳𝗋𝖺𝗇𝗌}\right]=\mathrm{V}\setminus \mathrm{ran}\left(\left(\mathrm{𝖲𝖲𝖾𝗍}\cap \left(\mathrm{𝖳𝗋𝖺𝗇𝗌}\times \mathrm{V}\right)\right)\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)$$
9	1 8	eqtr4i	$$⊢\mathrm{On}=\mathrm{V}\setminus \left(\mathrm{𝖲𝖲𝖾𝗍}\setminus \left(\mathrm{I}\cup \mathrm{E}\right)\right)\left[\mathrm{𝖳𝗋𝖺𝗇𝗌}\right]$$