regsfromregtr

	Ref	Expression
Hypotheses	regsfromregtr.1	$⊢ \exists y y \in w \to \exists y (y \in w \land \forall z (z \in y \to \neg z \in w))$
	regsfromregtr.2	$⊢ \exists u (v \in u \land \forall t (t \in u \to \forall s (s \in t \to s \in u)))$
Assertion	regsfromregtr	$⊢ \exists x φ \to \exists y (\forall x (x = y \to φ) \land \forall z (z \in y \to \neg \forall x (x = z \to φ)))$

Proof

Step	Hyp	Ref	Expression
1		regsfromregtr.1	$⊢ \exists y y \in w \to \exists y (y \in w \land \forall z (z \in y \to \neg z \in w))$
2		regsfromregtr.2	$⊢ \exists u (v \in u \land \forall t (t \in u \to \forall s (s \in t \to s \in u)))$
3		vex	$⊢ v \in V$
4		elequ1	$⊢ y = v \to (y \in u \leftrightarrow v \in u)$
5		sbequ	$⊢ y = v \to ([y/ x] φ \leftrightarrow [v/ x] φ)$
6	4 5	anbi12d	$⊢ y = v \to ((y \in u \land [y/ x] φ) \leftrightarrow (v \in u \land [v/ x] φ))$
7	3 6	spcev	$⊢ (v \in u \land [v/ x] φ) \to \exists y (y \in u \land [y/ x] φ)$
8	7	adantlr	$⊢ ((v \in u \land Tr u) \land [v/ x] φ) \to \exists y (y \in u \land [y/ x] φ)$
9		vex	$⊢ u \in V$
10	9	rabex	$⊢ \{r \in u \| [r/ x] φ\} \in V$
11		eleq2	$⊢ w = \{r \in u \| [r/ x] φ\} \to (y \in w \leftrightarrow y \in \{r \in u \| [r/ x] φ\})$
12		sbequ	$⊢ r = y \to ([r/ x] φ \leftrightarrow [y/ x] φ)$
13	12	elrab	$⊢ y \in \{r \in u \| [r/ x] φ\} \leftrightarrow (y \in u \land [y/ x] φ)$
14	11 13	bitrdi	$⊢ w = \{r \in u \| [r/ x] φ\} \to (y \in w \leftrightarrow (y \in u \land [y/ x] φ))$
15	14	exbidv	$⊢ w = \{r \in u \| [r/ x] φ\} \to (\exists y y \in w \leftrightarrow \exists y (y \in u \land [y/ x] φ))$
16		eleq2	$⊢ w = \{r \in u \| [r/ x] φ\} \to (z \in w \leftrightarrow z \in \{r \in u \| [r/ x] φ\})$
17		sbequ	$⊢ r = z \to ([r/ x] φ \leftrightarrow [z/ x] φ)$
18	17	elrab	$⊢ z \in \{r \in u \| [r/ x] φ\} \leftrightarrow (z \in u \land [z/ x] φ)$
19	16 18	bitrdi	$⊢ w = \{r \in u \| [r/ x] φ\} \to (z \in w \leftrightarrow (z \in u \land [z/ x] φ))$
20	19	notbid	$⊢ w = \{r \in u \| [r/ x] φ\} \to (\neg z \in w \leftrightarrow \neg (z \in u \land [z/ x] φ))$
21	20	imbi2d	$⊢ w = \{r \in u \| [r/ x] φ\} \to ((z \in y \to \neg z \in w) \leftrightarrow (z \in y \to \neg (z \in u \land [z/ x] φ)))$
22	21	albidv	$⊢ w = \{r \in u \| [r/ x] φ\} \to (\forall z (z \in y \to \neg z \in w) \leftrightarrow \forall z (z \in y \to \neg (z \in u \land [z/ x] φ)))$
23	14 22	anbi12d	$⊢ w = \{r \in u \| [r/ x] φ\} \to ((y \in w \land \forall z (z \in y \to \neg z \in w)) \leftrightarrow ((y \in u \land [y/ x] φ) \land \forall z (z \in y \to \neg (z \in u \land [z/ x] φ))))$
24	23	exbidv	$⊢ w = \{r \in u \| [r/ x] φ\} \to (\exists y (y \in w \land \forall z (z \in y \to \neg z \in w)) \leftrightarrow \exists y ((y \in u \land [y/ x] φ) \land \forall z (z \in y \to \neg (z \in u \land [z/ x] φ))))$
25	15 24	imbi12d	$⊢ w = \{r \in u \| [r/ x] φ\} \to ((\exists y y \in w \to \exists y (y \in w \land \forall z (z \in y \to \neg z \in w))) \leftrightarrow (\exists y (y \in u \land [y/ x] φ) \to \exists y ((y \in u \land [y/ x] φ) \land \forall z (z \in y \to \neg (z \in u \land [z/ x] φ)))))$
26	10 25 1	vtocl	$⊢ \exists y (y \in u \land [y/ x] φ) \to \exists y ((y \in u \land [y/ x] φ) \land \forall z (z \in y \to \neg (z \in u \land [z/ x] φ)))$
27	8 26	syl	$⊢ ((v \in u \land Tr u) \land [v/ x] φ) \to \exists y ((y \in u \land [y/ x] φ) \land \forall z (z \in y \to \neg (z \in u \land [z/ x] φ)))$
28		imnan	$⊢ (z \in u \to \neg [z/ x] φ) \leftrightarrow \neg (z \in u \land [z/ x] φ)$
29		trel	$⊢ Tr u \to ((z \in y \land y \in u) \to z \in u)$
30	29	imp	$⊢ (Tr u \land (z \in y \land y \in u)) \to z \in u$
31	30	anass1rs	$⊢ ((Tr u \land y \in u) \land z \in y) \to z \in u$
32		imbibi	$⊢ ((z \in u \to \neg [z/ x] φ) \leftrightarrow \neg (z \in u \land [z/ x] φ)) \to (z \in u \to (\neg [z/ x] φ \leftrightarrow \neg (z \in u \land [z/ x] φ)))$
33	28 31 32	mpsyl	$⊢ ((Tr u \land y \in u) \land z \in y) \to (\neg [z/ x] φ \leftrightarrow \neg (z \in u \land [z/ x] φ))$
34	33	pm5.74da	$⊢ (Tr u \land y \in u) \to ((z \in y \to \neg [z/ x] φ) \leftrightarrow (z \in y \to \neg (z \in u \land [z/ x] φ)))$
35	34	albidv	$⊢ (Tr u \land y \in u) \to (\forall z (z \in y \to \neg [z/ x] φ) \leftrightarrow \forall z (z \in y \to \neg (z \in u \land [z/ x] φ)))$
36	35	biimpar	$⊢ ((Tr u \land y \in u) \land \forall z (z \in y \to \neg (z \in u \land [z/ x] φ))) \to \forall z (z \in y \to \neg [z/ x] φ)$
37	36	anim2i	$⊢ ([y/ x] φ \land ((Tr u \land y \in u) \land \forall z (z \in y \to \neg (z \in u \land [z/ x] φ)))) \to ([y/ x] φ \land \forall z (z \in y \to \neg [z/ x] φ))$
38	37	exp44	$⊢ [y/ x] φ \to (Tr u \to (y \in u \to (\forall z (z \in y \to \neg (z \in u \land [z/ x] φ)) \to ([y/ x] φ \land \forall z (z \in y \to \neg [z/ x] φ)))))$
39	38	com3l	$⊢ Tr u \to (y \in u \to ([y/ x] φ \to (\forall z (z \in y \to \neg (z \in u \land [z/ x] φ)) \to ([y/ x] φ \land \forall z (z \in y \to \neg [z/ x] φ)))))$
40	39	imp4c	$⊢ Tr u \to (((y \in u \land [y/ x] φ) \land \forall z (z \in y \to \neg (z \in u \land [z/ x] φ))) \to ([y/ x] φ \land \forall z (z \in y \to \neg [z/ x] φ)))$
41	40	eximdv	$⊢ Tr u \to (\exists y ((y \in u \land [y/ x] φ) \land \forall z (z \in y \to \neg (z \in u \land [z/ x] φ))) \to \exists y ([y/ x] φ \land \forall z (z \in y \to \neg [z/ x] φ)))$
42	41	ad2antlr	$⊢ ((v \in u \land Tr u) \land [v/ x] φ) \to (\exists y ((y \in u \land [y/ x] φ) \land \forall z (z \in y \to \neg (z \in u \land [z/ x] φ))) \to \exists y ([y/ x] φ \land \forall z (z \in y \to \neg [z/ x] φ)))$
43	27 42	mpd	$⊢ ((v \in u \land Tr u) \land [v/ x] φ) \to \exists y ([y/ x] φ \land \forall z (z \in y \to \neg [z/ x] φ))$
44	43	ex	$⊢ (v \in u \land Tr u) \to ([v/ x] φ \to \exists y ([y/ x] φ \land \forall z (z \in y \to \neg [z/ x] φ)))$
45		dftr3	$⊢ Tr u \leftrightarrow \forall t \in u t \subseteq u$
46		df-ss	$⊢ t \subseteq u \leftrightarrow \forall s (s \in t \to s \in u)$
47	46	ralbii	$⊢ \forall t \in u t \subseteq u \leftrightarrow \forall t \in u \forall s (s \in t \to s \in u)$
48		df-ral	$⊢ \forall t \in u \forall s (s \in t \to s \in u) \leftrightarrow \forall t (t \in u \to \forall s (s \in t \to s \in u))$
49	45 47 48	3bitri	$⊢ Tr u \leftrightarrow \forall t (t \in u \to \forall s (s \in t \to s \in u))$
50	49	anbi2i	$⊢ (v \in u \land Tr u) \leftrightarrow (v \in u \land \forall t (t \in u \to \forall s (s \in t \to s \in u)))$
51	50	exbii	$⊢ \exists u (v \in u \land Tr u) \leftrightarrow \exists u (v \in u \land \forall t (t \in u \to \forall s (s \in t \to s \in u)))$
52	2 51	mpbir	$⊢ \exists u (v \in u \land Tr u)$
53	44 52	exlimiiv	$⊢ [v/ x] φ \to \exists y ([y/ x] φ \land \forall z (z \in y \to \neg [z/ x] φ))$
54	53	exlimiv	$⊢ \exists v [v/ x] φ \to \exists y ([y/ x] φ \land \forall z (z \in y \to \neg [z/ x] φ))$
55		nfv	$⊢ Ⅎ v φ$
56	55	sb8ef	$⊢ \exists x φ \leftrightarrow \exists v [v/ x] φ$
57	56	bicomi	$⊢ \exists v [v/ x] φ \leftrightarrow \exists x φ$
58		sb6	$⊢ [y/ x] φ \leftrightarrow \forall x (x = y \to φ)$
59		sb6	$⊢ [z/ x] φ \leftrightarrow \forall x (x = z \to φ)$
60	59	notbii	$⊢ \neg [z/ x] φ \leftrightarrow \neg \forall x (x = z \to φ)$
61	60	imbi2i	$⊢ (z \in y \to \neg [z/ x] φ) \leftrightarrow (z \in y \to \neg \forall x (x = z \to φ))$
62	61	albii	$⊢ \forall z (z \in y \to \neg [z/ x] φ) \leftrightarrow \forall z (z \in y \to \neg \forall x (x = z \to φ))$
63	58 62	anbi12i	$⊢ ([y/ x] φ \land \forall z (z \in y \to \neg [z/ x] φ)) \leftrightarrow (\forall x (x = y \to φ) \land \forall z (z \in y \to \neg \forall x (x = z \to φ)))$
64	63	exbii	$⊢ \exists y ([y/ x] φ \land \forall z (z \in y \to \neg [z/ x] φ)) \leftrightarrow \exists y (\forall x (x = y \to φ) \land \forall z (z \in y \to \neg \forall x (x = z \to φ)))$
65	54 57 64	3imtr3i	$⊢ \exists x φ \to \exists y (\forall x (x = y \to φ) \land \forall z (z \in y \to \neg \forall x (x = z \to φ)))$

Metamath Proof Explorer

Theorem regsfromregtr

Proof