Theorem srepdflem2 36005

Description: Lemma for srepdf 36006. (Contributed by BTernaryTau, 30-Sep-2026.)

Hypotheses

Ref	Expression
srepdflem2.1	⊢ Ⅎ𝑓𝜑
srepdflem2.2	⊢ Ⅎ𝑤𝜑
srepdflem2.3	⊢ Ⅎ𝑦𝜑
srepdflem2.4	⊢ Ⅎ𝑧𝜑
srepdflem2.5	⊢ (𝜑 → 𝑥 ∈ 𝑀)
srepdflem2.6	⊢ (𝜑 → (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))))
srepdflem2.7	⊢ (𝜑 → ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
srepdflem2.8	⊢ 𝐹 = (𝐺 ↾ 𝑥)
srepdflem2.9	⊢ 𝐺 = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}

Assertion

Ref	Expression
srepdflem2	⊢ (𝜑 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)))

Distinct variable groups:   𝑓,𝐹   𝑤,𝑓,𝑥,𝑦,𝑧   𝑓,𝑀,𝑤,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥, 𝑦, 𝑧, 𝑤, 𝑓)   𝜓(𝑥, 𝑦, 𝑧, 𝑤, 𝑓)   𝐹(𝑥, 𝑦, 𝑧, 𝑤)   𝐺(𝑥, 𝑦, 𝑧, 𝑤, 𝑓)   𝑀(𝑥)

Proof of Theorem srepdflem2

Step	Hyp	Ref	Expression
1		srepdflem2.8	. . . 4 ⊢ 𝐹 = (𝐺 ↾ 𝑥)
2		srepdflem2.7	. . . . 5 ⊢ (𝜑 → ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
3		nfa1 2187	. . . . . . . 8 ⊢ Ⅎ𝑦∀𝑦𝜓
4	3	rmo2i 3834	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓)
5	4	ralimi 3099	. . . . . 6 ⊢ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∀𝑤 ∈ 𝑀 ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓)
6		funopab 6575	. . . . . . 7 ⊢ (Fun {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)} ↔ ∀𝑤∃*𝑧(𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓))
7		srepdflem2.9	. . . . . . . 8 ⊢ 𝐺 = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}
8	7	funeqi 6560	. . . . . . 7 ⊢ (Fun 𝐺 ↔ Fun {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)})
9		2reu5lem2 3713	. . . . . . 7 ⊢ (∀𝑤 ∈ 𝑀 ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓 ↔ ∀𝑤∃*𝑧(𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓))
10	6, 8, 9	3bitr4i 306	. . . . . 6 ⊢ (Fun 𝐺 ↔ ∀𝑤 ∈ 𝑀 ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓)
11	5, 10	sylibr 237	. . . . 5 ⊢ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → Fun 𝐺)
12		resfunexg 7221	. . . . . 6 ⊢ ((Fun 𝐺 ∧ 𝑥 ∈ V) → (𝐺 ↾ 𝑥) ∈ V)
13	12	elvd 3456	. . . . 5 ⊢ (Fun 𝐺 → (𝐺 ↾ 𝑥) ∈ V)
14	2, 11, 13	3syl 19	. . . 4 ⊢ (𝜑 → (𝐺 ↾ 𝑥) ∈ V)
15	1, 14	eqeltrid 2864	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
16		srepdflem2.1	. . . 4 ⊢ Ⅎ𝑓𝜑
17		srepdflem2.2	. . . . . 6 ⊢ Ⅎ𝑤𝜑
18		srepdflem2.5	. . . . . . . 8 ⊢ (𝜑 → 𝑥 ∈ 𝑀)
19		elex2 2837	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑀 → ∃𝑦 𝑦 ∈ 𝑀)
20		rmoeq 3695	. . . . . . . . . 10 ⊢ ∃*𝑧 ∈ 𝑀 𝑧 = (𝑓‘𝑤)
21		simp3 1156	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → (𝑓‘𝑤) = 𝑧)
22	21	eqcomd 2766	. . . . . . . . . . . 12 ⊢ ((Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = (𝑓‘𝑤))
23	22	spsv 2019	. . . . . . . . . . 11 ⊢ (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = (𝑓‘𝑤))
24	23	rmoimi 3699	. . . . . . . . . 10 ⊢ (∃*𝑧 ∈ 𝑀 𝑧 = (𝑓‘𝑤) → ∃*𝑧 ∈ 𝑀 ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))
25	20, 24	ax-mp 5	. . . . . . . . 9 ⊢ ∃*𝑧 ∈ 𝑀 ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)
26		nfa1 2187	. . . . . . . . . 10 ⊢ Ⅎ𝑦∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)
27	26	rmo6 35756	. . . . . . . . 9 ⊢ (∃*𝑧 ∈ 𝑀 ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) ↔ (∃𝑦 𝑦 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦)))
28	25, 27	mpbi 233	. . . . . . . 8 ⊢ (∃𝑦 𝑦 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦))
29	18, 19, 28	3syl 19	. . . . . . 7 ⊢ (𝜑 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦))
30	29	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑀) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦))
31	17, 30	ralrimia 3261	. . . . 5 ⊢ (𝜑 → ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦))
32		srepdflem2.6	. . . . 5 ⊢ (𝜑 → (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))))
33	31, 32	mpd 16	. . . 4 ⊢ (𝜑 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))))
34	16, 33	alrimi 2249	. . 3 ⊢ (𝜑 → ∀𝑓∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))))
35		nfv 1946	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑤 ∈ 𝑀
36		nfv 1946	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑧 ∈ 𝑀
37	35, 36, 3	nf3an 1933	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)
38	37	nfopab 5173	. . . . . . . . 9 ⊢ Ⅎ𝑦{⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}
39	7, 38	nfcxfr 2920	. . . . . . . 8 ⊢ Ⅎ𝑦𝐺
40		nfcv 2922	. . . . . . . 8 ⊢ Ⅎ𝑦𝑥
41	39, 40	nfres 5971	. . . . . . 7 ⊢ Ⅎ𝑦(𝐺 ↾ 𝑥)
42	1, 41	nfcxfr 2920	. . . . . 6 ⊢ Ⅎ𝑦𝐹
43	42	nfeq2 2939	. . . . 5 ⊢ Ⅎ𝑦 𝑓 = 𝐹
44		nfopab2 5175	. . . . . . . . . 10 ⊢ Ⅎ𝑧{⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}
45	7, 44	nfcxfr 2920	. . . . . . . . 9 ⊢ Ⅎ𝑧𝐺
46		nfcv 2922	. . . . . . . . 9 ⊢ Ⅎ𝑧𝑥
47	45, 46	nfres 5971	. . . . . . . 8 ⊢ Ⅎ𝑧(𝐺 ↾ 𝑥)
48	1, 47	nfcxfr 2920	. . . . . . 7 ⊢ Ⅎ𝑧𝐹
49	48	nfeq2 2939	. . . . . 6 ⊢ Ⅎ𝑧 𝑓 = 𝐹
50		nfopab1 5174	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤{⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}
51	7, 50	nfcxfr 2920	. . . . . . . . . . 11 ⊢ Ⅎ𝑤𝐺
52		nfcv 2922	. . . . . . . . . . 11 ⊢ Ⅎ𝑤𝑥
53	51, 52	nfres 5971	. . . . . . . . . 10 ⊢ Ⅎ𝑤(𝐺 ↾ 𝑥)
54	1, 53	nfcxfr 2920	. . . . . . . . 9 ⊢ Ⅎ𝑤𝐹
55	54	nfeq2 2939	. . . . . . . 8 ⊢ Ⅎ𝑤 𝑓 = 𝐹
56		funeq 6559	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (Fun 𝑓 ↔ Fun 𝐹))
57		dmeq 5884	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
58	57	eleq2d 2846	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑤 ∈ dom 𝑓 ↔ 𝑤 ∈ dom 𝐹))
59		fveq1 6884	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑤) = (𝐹‘𝑤))
60	59	eqeq1d 2762	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑤) = 𝑧 ↔ (𝐹‘𝑤) = 𝑧))
61	56, 58, 60	3anbi123d 1464	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → ((Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) ↔ (Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
62	43, 61	albid 2258	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) ↔ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
63	62	anbi2d 642	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → ((𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)) ↔ (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))))
64	55, 63	rexbid 3276	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)) ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))))
65	64	bibi2d 345	. . . . . 6 ⊢ (𝑓 = 𝐹 → ((𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))) ↔ (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))))
66	49, 65	ralbid 3275	. . . . 5 ⊢ (𝑓 = 𝐹 → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))))
67	43, 66	rexbid 3276	. . . 4 ⊢ (𝑓 = 𝐹 → (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))) ↔ ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))))
68	67	spcgv 3550	. . 3 ⊢ (𝐹 ∈ V → (∀𝑓∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))))
69	15, 34, 68	sylc 66	. 2 ⊢ (𝜑 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))))
70		srepdflem2.3	. . 3 ⊢ Ⅎ𝑦𝜑
71		srepdflem2.4	. . . . 5 ⊢ Ⅎ𝑧𝜑
72	17, 2, 1, 7	srepdflem1 36004	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → (∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))))
73		biantr 818	. . . . . . 7 ⊢ (((𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))) ∧ (∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))) → (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)))
74	72, 73	sylan2 605	. . . . . 6 ⊢ (((𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))) ∧ (𝜑 ∧ 𝑧 ∈ 𝑀)) → (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)))
75	74	expcom 419	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → ((𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))) → (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓))))
76	71, 75	ralimdaa 3263	. . . 4 ⊢ (𝜑 → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))) → ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓))))
77	76	a1d 26	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝑀 → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))) → ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)))))
78	70, 77	reximdai 3264	. 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓))))
79	69, 78	mpd 16	1 ⊢ (𝜑 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103  ∀wal 1567   = wceq 1569  ∃wex 1811  Ⅎwnf 1815   ∈ wcel 2144  ∃*wmo 2562  ∀wral 3076  ∃wrex 3086  ∃*wrmo 3364  Vcvv 3450  {copab 5166  dom cdm 5650   ↾ cres 5652  Fun wfun 6532  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546

This theorem is used by:  srepdf  36006