srepdflem2

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

Proof

Step	Hyp	Ref	Expression
1		srepdflem2.1	$⊢ Ⅎ f φ$
2		srepdflem2.2	$⊢ Ⅎ w φ$
3		srepdflem2.3	$⊢ Ⅎ y φ$
4		srepdflem2.4	$⊢ Ⅎ z φ$
5		srepdflem2.5	$⊢ φ \to x \in M$
6		srepdflem2.6	$⊢ φ \to (\forall w \in M \exists y \in M \forall z \in M (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y) \to \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))))$
7		srepdflem2.7	$⊢ φ \to \forall w \in M \exists y \in M \forall z \in M (\forall y ψ \to z = y)$
8		srepdflem2.8	$⊢ F = {G ↾}_{x}$
9		srepdflem2.9	$⊢ G = \{⟨w, z⟩ \| (w \in M \land z \in M \land \forall y ψ)\}$
10		nfa1	$⊢ Ⅎ y \forall y ψ$
11	10	rmo2i	$⊢ \exists y \in M \forall z \in M (\forall y ψ \to z = y) \to \exists^{*} z \in M \forall y ψ$
12	11	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 ψ$
13		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 ψ)$
14	9	funeqi	$⊢ Fun G \leftrightarrow Fun \{⟨w, z⟩ \| (w \in M \land z \in M \land \forall y ψ)\}$
15		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 ψ)$
16	13 14 15	3bitr4i	$⊢ Fun G \leftrightarrow \forall w \in M \exists^{*} z \in M \forall y ψ$
17	12 16	sylibr	$⊢ \forall w \in M \exists y \in M \forall z \in M (\forall y ψ \to z = y) \to Fun G$
18		resfunexg	$⊢ (Fun G \land x \in V) \to {G ↾}_{x} \in V$
19	18	elvd	$⊢ Fun G \to {G ↾}_{x} \in V$
20	7 17 19	3syl	$⊢ φ \to {G ↾}_{x} \in V$
21	8 20	eqeltrid	$⊢ φ \to F \in V$
22		elex2	$⊢ x \in M \to \exists y y \in M$
23		rmoeq	$⊢ \exists^{*} z \in M z = f (w)$
24		simp3	$⊢ (Fun f \land w \in dom f \land f (w) = z) \to f (w) = z$
25	24	eqcomd	$⊢ (Fun f \land w \in dom f \land f (w) = z) \to z = f (w)$
26	25	spsv	$⊢ \forall y (Fun f \land w \in dom f \land f (w) = z) \to z = f (w)$
27	26	rmoimi	$⊢ \exists^{} z \in M z = f (w) \to \exists^{} z \in M \forall y (Fun f \land w \in dom f \land f (w) = z)$
28	23 27	ax-mp	$⊢ \exists^{*} z \in M \forall y (Fun f \land w \in dom f \land f (w) = z)$
29		nfa1	$⊢ Ⅎ y \forall y (Fun f \land w \in dom f \land f (w) = z)$
30	29	rmo6	$⊢ \exists^{*} z \in M \forall y (Fun f \land w \in dom f \land f (w) = z) \leftrightarrow (\exists y y \in M \to \exists y \in M \forall z \in M (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y))$
31	28 30	mpbi	$⊢ \exists y y \in M \to \exists y \in M \forall z \in M (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
32	5 22 31	3syl	$⊢ φ \to \exists y \in M \forall z \in M (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
33	32	adantr	$⊢ (φ \land w \in M) \to \exists y \in M \forall z \in M (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
34	2 33	ralrimia	$⊢ φ \to \forall w \in M \exists y \in M \forall z \in M (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
35	34 6	mpd	$⊢ φ \to \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)))$
36	1 35	alrimi	$⊢ φ \to \forall f \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)))$
37		nfv	$⊢ Ⅎ y w \in M$
38		nfv	$⊢ Ⅎ y z \in M$
39	37 38 10	nf3an	$⊢ Ⅎ y (w \in M \land z \in M \land \forall y ψ)$
40	39	nfopab	$⊢ \underline{Ⅎ} y \{⟨w, z⟩ \| (w \in M \land z \in M \land \forall y ψ)\}$
41	9 40	nfcxfr	$⊢ \underline{Ⅎ} y G$
42		nfcv	$⊢ \underline{Ⅎ} y x$
43	41 42	nfres	$⊢ \underline{Ⅎ} y ({G ↾}_{x})$
44	8 43	nfcxfr	$⊢ \underline{Ⅎ} y F$
45	44	nfeq2	$⊢ Ⅎ y f = F$
46		nfopab2	$⊢ \underline{Ⅎ} z \{⟨w, z⟩ \| (w \in M \land z \in M \land \forall y ψ)\}$
47	9 46	nfcxfr	$⊢ \underline{Ⅎ} z G$
48		nfcv	$⊢ \underline{Ⅎ} z x$
49	47 48	nfres	$⊢ \underline{Ⅎ} z ({G ↾}_{x})$
50	8 49	nfcxfr	$⊢ \underline{Ⅎ} z F$
51	50	nfeq2	$⊢ Ⅎ z f = F$
52		nfopab1	$⊢ \underline{Ⅎ} w \{⟨w, z⟩ \| (w \in M \land z \in M \land \forall y ψ)\}$
53	9 52	nfcxfr	$⊢ \underline{Ⅎ} w G$
54		nfcv	$⊢ \underline{Ⅎ} w x$
55	53 54	nfres	$⊢ \underline{Ⅎ} w ({G ↾}_{x})$
56	8 55	nfcxfr	$⊢ \underline{Ⅎ} w F$
57	56	nfeq2	$⊢ Ⅎ w f = F$
58		funeq	$⊢ f = F \to (Fun f \leftrightarrow Fun F)$
59		dmeq	$⊢ f = F \to dom f = dom F$
60	59	eleq2d	$⊢ f = F \to (w \in dom f \leftrightarrow w \in dom F)$
61		fveq1	$⊢ f = F \to f (w) = F (w)$
62	61	eqeq1d	$⊢ f = F \to (f (w) = z \leftrightarrow F (w) = z)$
63	58 60 62	3anbi123d	$⊢ f = F \to ((Fun f \land w \in dom f \land f (w) = z) \leftrightarrow (Fun F \land w \in dom F \land F (w) = z))$
64	45 63	albid	$⊢ f = F \to (\forall y (Fun f \land w \in dom f \land f (w) = z) \leftrightarrow \forall y (Fun F \land w \in dom F \land F (w) = z))$
65	64	anbi2d	$⊢ f = F \to ((w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)) \leftrightarrow (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z)))$
66	57 65	rexbid	$⊢ f = F \to (\exists w \in M (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)) \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z)))$
67	66	bibi2d	$⊢ f = F \to ((z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))) \leftrightarrow (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z))))$
68	51 67	ralbid	$⊢ f = F \to (\forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))) \leftrightarrow \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z))))$
69	45 68	rexbid	$⊢ f = F \to (\exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))) \leftrightarrow \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z))))$
70	69	spcgv	$⊢ F \in V \to (\forall f \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))) \to \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z))))$
71	21 36 70	sylc	$⊢ φ \to \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z)))$
72	2 7 8 9	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)))$
73		biantr	$⊢ ((z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z))) \land (\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)))) \to (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y ψ))$
74	72 73	sylan2	$⊢ ((z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z))) \land (φ \land z \in M)) \to (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y ψ))$
75	74	expcom	$⊢ (φ \land z \in M) \to ((z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z))) \to (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y ψ)))$
76	4 75	ralimdaa	$⊢ φ \to (\forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z))) \to \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y ψ)))$
77	76	a1d	$⊢ φ \to (y \in M \to (\forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z))) \to \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y ψ))))$
78	3 77	reximdai	$⊢ φ \to (\exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun F \land w \in dom F \land F (w) = z))) \to \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y ψ)))$
79	71 78	mpd	$⊢ φ \to \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y ψ))$

Metamath Proof Explorer

Theorem srepdflem2

Proof