srepdflem1

	Ref	Expression
Hypotheses	srepdflem1.1	$⊢ Ⅎ w φ$
	srepdflem1.2	$⊢ φ \to \forall w \in M \exists y \in M \forall z \in M (\forall y ψ \to z = y)$
	srepdflem1.3	$⊢ F = {G ↾}_{x}$
	srepdflem1.4	$⊢ G = \{⟨w, z⟩ \| (w \in M \land z \in M \land \forall y ψ)\}$
Assertion	srepdflem1	$⊢ (φ \land z \in M) \to (\exists w \in M (w \in x \land \forall y ψ) \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z)))$

Proof

Step	Hyp	Ref	Expression
1		srepdflem1.1	$⊢ Ⅎ w φ$
2		srepdflem1.2	$⊢ φ \to \forall w \in M \exists y \in M \forall z \in M (\forall y ψ \to z = y)$
3		srepdflem1.3	$⊢ F = {G ↾}_{x}$
4		srepdflem1.4	$⊢ G = \{⟨w, z⟩ \| (w \in M \land z \in M \land \forall y ψ)\}$
5		nfv	$⊢ Ⅎ w z \in M$
6	1 5	nfan	$⊢ Ⅎ w (φ \land z \in M)$
7		3anass	$⊢ (w \in M \land w \in x \land \forall y ψ) \leftrightarrow (w \in M \land (w \in x \land \forall y ψ))$
8	7	baibr	$⊢ w \in M \to ((w \in x \land \forall y ψ) \leftrightarrow (w \in M \land w \in x \land \forall y ψ))$
9		simp2	$⊢ (w \in M \land w \in x \land \forall y ψ) \to w \in x$
10	9	a1i	$⊢ (φ \land z \in M) \to ((w \in M \land w \in x \land \forall y ψ) \to w \in x)$
11		ibar	$⊢ z \in M \to ((w \in M \land w \in x \land \forall y ψ) \leftrightarrow (z \in M \land (w \in M \land w \in x \land \forall y ψ)))$
12		nfa1	$⊢ Ⅎ y \forall y ψ$
13		rexex	$⊢ \exists y \in M \forall z \in M (\forall y ψ \to z = y) \to \exists y \forall z \in M (\forall y ψ \to z = y)$
14	13	ralimi	$⊢ \forall w \in M \exists y \in M \forall z \in M (\forall y ψ \to z = y) \to \forall w \in M \exists y \forall z \in M (\forall y ψ \to z = y)$
15	2 14	syl	$⊢ φ \to \forall w \in M \exists y \forall z \in M (\forall y ψ \to z = y)$
16	4	reseq1i	$⊢ {G ↾}_{x} = {\{⟨w, z⟩ \| (w \in M \land z \in M \land \forall y ψ)\} ↾}_{x}$
17	3 16	eqtri	$⊢ F = {\{⟨w, z⟩ \| (w \in M \land z \in M \land \forall y ψ)\} ↾}_{x}$
18	12 15 17	fwfffunres	$⊢ φ \to ((z \in M \land (w \in M \land w \in x \land \forall y ψ)) \leftrightarrow (w \in dom F \land F (w) = z))$
19	12	rmo2i	$⊢ \exists y \in M \forall z \in M (\forall y ψ \to z = y) \to \exists^{*} z \in M \forall y ψ$
20	19	ralimi	$⊢ \forall w \in M \exists y \in M \forall z \in M (\forall y ψ \to z = y) \to \forall w \in M \exists^{*} z \in M \forall y ψ$
21		funopab	$⊢ Fun \{⟨w, z⟩ \| (w \in M \land z \in M \land \forall y ψ)\} \leftrightarrow \forall w \exists^{*} z (w \in M \land z \in M \land \forall y ψ)$
22	4	funeqi	$⊢ Fun G \leftrightarrow Fun \{⟨w, z⟩ \| (w \in M \land z \in M \land \forall y ψ)\}$
23		2reu5lem2	$⊢ \forall w \in M \exists^{} z \in M \forall y ψ \leftrightarrow \forall w \exists^{} z (w \in M \land z \in M \land \forall y ψ)$
24	21 22 23	3bitr4i	$⊢ Fun G \leftrightarrow \forall w \in M \exists^{*} z \in M \forall y ψ$
25	20 24	sylibr	$⊢ \forall w \in M \exists y \in M \forall z \in M (\forall y ψ \to z = y) \to Fun G$
26		funres	$⊢ Fun G \to Fun ({G ↾}_{x})$
27	2 25 26	3syl	$⊢ φ \to Fun ({G ↾}_{x})$
28	3	funeqi	$⊢ Fun F \leftrightarrow Fun ({G ↾}_{x})$
29	27 28	sylibr	$⊢ φ \to Fun F$
30	29	3biant1d	$⊢ φ \to ((w \in dom F \land F (w) = z) \leftrightarrow (Fun F \land w \in dom F \land F (w) = z))$
31	18 30	bitrd	$⊢ φ \to ((z \in M \land (w \in M \land w \in x \land \forall y ψ)) \leftrightarrow (Fun F \land w \in dom F \land F (w) = z))$
32	11 31	sylan9bbr	$⊢ (φ \land z \in M) \to ((w \in M \land w \in x \land \forall y ψ) \leftrightarrow (Fun F \land w \in dom F \land F (w) = z))$
33		nfv	$⊢ Ⅎ y w \in M$
34		nfv	$⊢ Ⅎ y z \in M$
35	33 34 12	nf3an	$⊢ Ⅎ y (w \in M \land z \in M \land \forall y ψ)$
36	35	nfopab	$⊢ \underline{Ⅎ} y \{⟨w, z⟩ \| (w \in M \land z \in M \land \forall y ψ)\}$
37	4 36	nfcxfr	$⊢ \underline{Ⅎ} y G$
38		nfcv	$⊢ \underline{Ⅎ} y x$
39	37 38	nfres	$⊢ \underline{Ⅎ} y ({G ↾}_{x})$
40	3 39	nfcxfr	$⊢ \underline{Ⅎ} y F$
41	40	nffun	$⊢ Ⅎ y Fun F$
42	40	nfdm	$⊢ \underline{Ⅎ} y dom F$
43	42	nfcri	$⊢ Ⅎ y w \in dom F$
44		nfcv	$⊢ \underline{Ⅎ} y w$
45	40 44	nffv	$⊢ \underline{Ⅎ} y F (w)$
46	45	nfeq1	$⊢ Ⅎ y F (w) = z$
47	41 43 46	nf3an	$⊢ Ⅎ y (Fun F \land w \in dom F \land F (w) = z)$
48	47	19.3	$⊢ \forall y (Fun F \land w \in dom F \land F (w) = z) \leftrightarrow (Fun F \land w \in dom F \land F (w) = z)$
49	32 48	bitr4di	$⊢ (φ \land z \in M) \to ((w \in M \land w \in x \land \forall y ψ) \leftrightarrow \forall y (Fun F \land w \in dom F \land F (w) = z))$
50	49	biimpd	$⊢ (φ \land z \in M) \to ((w \in M \land w \in x \land \forall y ψ) \to \forall y (Fun F \land w \in dom F \land F (w) = z))$
51	10 50	jcad	$⊢ (φ \land z \in M) \to ((w \in M \land w \in x \land \forall y ψ) \to (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z)))$
52	49	biimprd	$⊢ (φ \land z \in M) \to (\forall y (Fun F \land w \in dom F \land F (w) = z) \to (w \in M \land w \in x \land \forall y ψ))$
53	52	adantld	$⊢ (φ \land z \in M) \to ((w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z)) \to (w \in M \land w \in x \land \forall y ψ))$
54	51 53	impbid	$⊢ (φ \land z \in M) \to ((w \in M \land w \in x \land \forall y ψ) \leftrightarrow (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z)))$
55	8 54	sylan9bbr	$⊢ ((φ \land z \in M) \land w \in M) \to ((w \in x \land \forall y ψ) \leftrightarrow (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z)))$
56	6 55	rexbida	$⊢ (φ \land z \in M) \to (\exists w \in M (w \in x \land \forall y ψ) \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z)))$

Metamath Proof Explorer

Theorem srepdflem1

Proof