dfon3

Description: A quantifier-free definition of On . (Contributed by Scott Fenton, 5-Apr-2012)

		Ref	Expression
	Assertion	dfon3	$⊢ On = V ∖ ran ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E))$

Proof

Step	Hyp	Ref	Expression
1		dfon2	$⊢ On = \{x \| \forall y ((y \subset x \land Tr y) \to y \in x)\}$
2		abeq1	$⊢ \{x \| \forall y ((y \subset x \land Tr y) \to y \in x)\} = V ∖ ran ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E)) \leftrightarrow \forall x (\forall y ((y \subset x \land Tr y) \to y \in x) \leftrightarrow x \in (V ∖ ran ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E))))$
3		vex	$⊢ x \in V$
4	3	elrn	$⊢ x \in ran ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E)) \leftrightarrow \exists y y ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E)) x$
5		brin	$⊢ y (𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) x \leftrightarrow (y 𝖲𝖲𝖾𝗍 x \land y (𝖳𝗋𝖺𝗇𝗌 \times V) x)$
6	3	brsset	$⊢ y 𝖲𝖲𝖾𝗍 x \leftrightarrow y \subseteq x$
7		brxp	$⊢ y (𝖳𝗋𝖺𝗇𝗌 \times V) x \leftrightarrow (y \in 𝖳𝗋𝖺𝗇𝗌 \land x \in V)$
8	3 7	mpbiran2	$⊢ y (𝖳𝗋𝖺𝗇𝗌 \times V) x \leftrightarrow y \in 𝖳𝗋𝖺𝗇𝗌$
9		vex	$⊢ y \in V$
10	9	eltrans	$⊢ y \in 𝖳𝗋𝖺𝗇𝗌 \leftrightarrow Tr y$
11	8 10	bitri	$⊢ y (𝖳𝗋𝖺𝗇𝗌 \times V) x \leftrightarrow Tr y$
12	6 11	anbi12i	$⊢ (y 𝖲𝖲𝖾𝗍 x \land y (𝖳𝗋𝖺𝗇𝗌 \times V) x) \leftrightarrow (y \subseteq x \land Tr y)$
13	5 12	bitri	$⊢ y (𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) x \leftrightarrow (y \subseteq x \land Tr y)$
14		ioran	$⊢ \neg (y = x \lor y \in x) \leftrightarrow (\neg y = x \land \neg y \in x)$
15		brun	$⊢ y (I \cup E) x \leftrightarrow (y I x \lor y E x)$
16	3	ideq	$⊢ y I x \leftrightarrow y = x$
17		epel	$⊢ y E x \leftrightarrow y \in x$
18	16 17	orbi12i	$⊢ (y I x \lor y E x) \leftrightarrow (y = x \lor y \in x)$
19	15 18	bitri	$⊢ y (I \cup E) x \leftrightarrow (y = x \lor y \in x)$
20	14 19	xchnxbir	$⊢ \neg y (I \cup E) x \leftrightarrow (\neg y = x \land \neg y \in x)$
21	13 20	anbi12i	$⊢ (y (𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) x \land \neg y (I \cup E) x) \leftrightarrow ((y \subseteq x \land Tr y) \land (\neg y = x \land \neg y \in x))$
22		brdif	$⊢ y ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E)) x \leftrightarrow (y (𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) x \land \neg y (I \cup E) x)$
23		dfpss2	$⊢ y \subset x \leftrightarrow (y \subseteq x \land \neg y = x)$
24	23	anbi1i	$⊢ (y \subset x \land Tr y) \leftrightarrow ((y \subseteq x \land \neg y = x) \land Tr y)$
25		an32	$⊢ ((y \subseteq x \land \neg y = x) \land Tr y) \leftrightarrow ((y \subseteq x \land Tr y) \land \neg y = x)$
26	24 25	bitri	$⊢ (y \subset x \land Tr y) \leftrightarrow ((y \subseteq x \land Tr y) \land \neg y = x)$
27	26	anbi1i	$⊢ ((y \subset x \land Tr y) \land \neg y \in x) \leftrightarrow (((y \subseteq x \land Tr y) \land \neg y = x) \land \neg y \in x)$
28		anass	$⊢ (((y \subseteq x \land Tr y) \land \neg y = x) \land \neg y \in x) \leftrightarrow ((y \subseteq x \land Tr y) \land (\neg y = x \land \neg y \in x))$
29	27 28	bitri	$⊢ ((y \subset x \land Tr y) \land \neg y \in x) \leftrightarrow ((y \subseteq x \land Tr y) \land (\neg y = x \land \neg y \in x))$
30	21 22 29	3bitr4i	$⊢ y ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E)) x \leftrightarrow ((y \subset x \land Tr y) \land \neg y \in x)$
31	30	exbii	$⊢ \exists y y ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E)) x \leftrightarrow \exists y ((y \subset x \land Tr y) \land \neg y \in x)$
32		exanali	$⊢ \exists y ((y \subset x \land Tr y) \land \neg y \in x) \leftrightarrow \neg \forall y ((y \subset x \land Tr y) \to y \in x)$
33	31 32	bitri	$⊢ \exists y y ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E)) x \leftrightarrow \neg \forall y ((y \subset x \land Tr y) \to y \in x)$
34	4 33	bitri	$⊢ x \in ran ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E)) \leftrightarrow \neg \forall y ((y \subset x \land Tr y) \to y \in x)$
35	34	con2bii	$⊢ \forall y ((y \subset x \land Tr y) \to y \in x) \leftrightarrow \neg x \in ran ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E))$
36		eldif	$⊢ x \in (V ∖ ran ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E))) \leftrightarrow (x \in V \land \neg x \in ran ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E)))$
37	3 36	mpbiran	$⊢ x \in (V ∖ ran ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E))) \leftrightarrow \neg x \in ran ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E))$
38	35 37	bitr4i	$⊢ \forall y ((y \subset x \land Tr y) \to y \in x) \leftrightarrow x \in (V ∖ ran ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E)))$
39	2 38	mpgbir	$⊢ \{x \| \forall y ((y \subset x \land Tr y) \to y \in x)\} = V ∖ ran ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E))$
40	1 39	eqtri	$⊢ On = V ∖ ran ((𝖲𝖲𝖾𝗍 \cap (𝖳𝗋𝖺𝗇𝗌 \times V)) ∖ (I \cup E))$

Metamath Proof Explorer

Theorem dfon3

Proof