dfon4

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

		Ref	Expression
	Assertion	dfon4	$⊢ On = V ∖ (𝖲𝖲𝖾𝗍 ∖ (I \cup E)) [𝖳𝗋𝖺𝗇𝗌]$

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

Metamath Proof Explorer