Theorem srepdflem2 36086

Description: Lemma for srepdf 36087. (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 2191	. . . . . . . 8 ⊢ Ⅎ𝑦∀𝑦𝜓
4	3	rmo2i 3839	. . . . . . 7 ⊢ (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓)
5	4	ralimi 3103	. . . . . 6 ⊢ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∀𝑤 ∈ 𝑀 ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓)
6		funopab 6595	. . . . . . 7 ⊢ (Fun {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)} ↔ ∀𝑤∃*𝑧(𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓))
7		srepdflem2.9	. . . . . . . 8 ⊢ 𝐺 = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}
8	7	funeqi 6580	. . . . . . 7 ⊢ (Fun 𝐺 ↔ Fun {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)})
9		2reu5lem2 3717	. . . . . . 7 ⊢ (∀𝑤 ∈ 𝑀 ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓 ↔ ∀𝑤∃*𝑧(𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓))
10	6, 8, 9	3bitr4i 306	. . . . . 6 ⊢ (Fun 𝐺 ↔ ∀𝑤 ∈ 𝑀 ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓)
11	5, 10	sylibr 237	. . . . 5 ⊢ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → Fun 𝐺)
12		resfunexg 7244	. . . . . 6 ⊢ ((Fun 𝐺 ∧ 𝑥 ∈ V) → (𝐺 ↾ 𝑥) ∈ V)
13	12	elvd 3460	. . . . 5 ⊢ (Fun 𝐺 → (𝐺 ↾ 𝑥) ∈ V)
14	2, 11, 13	3syl 19	. . . 4 ⊢ (𝜑 → (𝐺 ↾ 𝑥) ∈ V)
15	1, 14	eqeltrid 2868	. . 3 ⊢ (𝜑 → 𝐹 ∈ V)
16		srepdflem2.1	. . . 4 ⊢ Ⅎ𝑓𝜑
17		srepdflem2.2	. . . . . 6 ⊢ Ⅎ𝑤𝜑
18		srepdflem2.5	. . . . . . . 8 ⊢ (𝜑 → 𝑥 ∈ 𝑀)
19		elex2 2841	. . . . . . . 8 ⊢ (𝑥 ∈ 𝑀 → ∃𝑦 𝑦 ∈ 𝑀)
20		rmoeq 3699	. . . . . . . . . 10 ⊢ ∃*𝑧 ∈ 𝑀 𝑧 = (𝑓‘𝑤)
21		simp3 1156	. . . . . . . . . . . . 13 ⊢ ((Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → (𝑓‘𝑤) = 𝑧)
22	21	eqcomd 2769	. . . . . . . . . . . 12 ⊢ ((Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = (𝑓‘𝑤))
23	22	spsv 2022	. . . . . . . . . . 11 ⊢ (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = (𝑓‘𝑤))
24	23	rmoimi 3703	. . . . . . . . . 10 ⊢ (∃*𝑧 ∈ 𝑀 𝑧 = (𝑓‘𝑤) → ∃*𝑧 ∈ 𝑀 ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))
25	20, 24	ax-mp 5	. . . . . . . . 9 ⊢ ∃*𝑧 ∈ 𝑀 ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)
26		nfa1 2191	. . . . . . . . . 10 ⊢ Ⅎ𝑦∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)
27	26	rmo6 35780	. . . . . . . . 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 3265	. . . . 5 ⊢ (𝜑 → ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦))
32		srepdflem2.6	. . . . 5 ⊢ (𝜑 → (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))))
33	31, 32	mpd 16	. . . 4 ⊢ (𝜑 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))))
34	16, 33	alrimi 2253	. . 3 ⊢ (𝜑 → ∀𝑓∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))))
35		nfv 1949	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑤 ∈ 𝑀
36		nfv 1949	. . . . . . . . . . 11 ⊢ Ⅎ𝑦 𝑧 ∈ 𝑀
37	35, 36, 3	nf3an 1936	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)
38	37	nfopab 5177	. . . . . . . . 9 ⊢ Ⅎ𝑦{⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}
39	7, 38	nfcxfr 2924	. . . . . . . 8 ⊢ Ⅎ𝑦𝐺
40		nfcv 2926	. . . . . . . 8 ⊢ Ⅎ𝑦𝑥
41	39, 40	nfres 5983	. . . . . . 7 ⊢ Ⅎ𝑦(𝐺 ↾ 𝑥)
42	1, 41	nfcxfr 2924	. . . . . 6 ⊢ Ⅎ𝑦𝐹
43	42	nfeq2 2943	. . . . 5 ⊢ Ⅎ𝑦 𝑓 = 𝐹
44		nfopab2 5179	. . . . . . . . . 10 ⊢ Ⅎ𝑧{⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}
45	7, 44	nfcxfr 2924	. . . . . . . . 9 ⊢ Ⅎ𝑧𝐺
46		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑧𝑥
47	45, 46	nfres 5983	. . . . . . . 8 ⊢ Ⅎ𝑧(𝐺 ↾ 𝑥)
48	1, 47	nfcxfr 2924	. . . . . . 7 ⊢ Ⅎ𝑧𝐹
49	48	nfeq2 2943	. . . . . 6 ⊢ Ⅎ𝑧 𝑓 = 𝐹
50		nfopab1 5178	. . . . . . . . . . . 12 ⊢ Ⅎ𝑤{⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}
51	7, 50	nfcxfr 2924	. . . . . . . . . . 11 ⊢ Ⅎ𝑤𝐺
52		nfcv 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑤𝑥
53	51, 52	nfres 5983	. . . . . . . . . 10 ⊢ Ⅎ𝑤(𝐺 ↾ 𝑥)
54	1, 53	nfcxfr 2924	. . . . . . . . 9 ⊢ Ⅎ𝑤𝐹
55	54	nfeq2 2943	. . . . . . . 8 ⊢ Ⅎ𝑤 𝑓 = 𝐹
56		funeq 6579	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (Fun 𝑓 ↔ Fun 𝐹))
57		dmeq 5892	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹)
58	57	eleq2d 2850	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → (𝑤 ∈ dom 𝑓 ↔ 𝑤 ∈ dom 𝐹))
59		fveq1 6907	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑤) = (𝐹‘𝑤))
60	59	eqeq1d 2765	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑤) = 𝑧 ↔ (𝐹‘𝑤) = 𝑧))
61	56, 58, 60	3anbi123d 1465	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → ((Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) ↔ (Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
62	43, 61	albid 2262	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) ↔ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
63	62	anbi2d 642	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → ((𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)) ↔ (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))))
64	55, 63	rexbid 3280	. . . . . . 7 ⊢ (𝑓 = 𝐹 → (∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)) ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))))
65	64	bibi2d 345	. . . . . 6 ⊢ (𝑓 = 𝐹 → ((𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))) ↔ (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))))
66	49, 65	ralbid 3279	. . . . 5 ⊢ (𝑓 = 𝐹 → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))) ↔ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))))
67	43, 66	rexbid 3280	. . . 4 ⊢ (𝑓 = 𝐹 → (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))) ↔ ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))))
68	67	spcgv 3554	. . 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 36085	. . . . . . 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 3267	. . . 4 ⊢ (𝜑 → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))) → ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓))))
77	76	a1d 26	. . 3 ⊢ (𝜑 → (𝑦 ∈ 𝑀 → (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))) → ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)))))
78	70, 77	reximdai 3268	. 2 ⊢ (𝜑 → (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓))))
79	69, 78	mpd 16	1 ⊢ (𝜑 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103  ∀wal 1568   = wceq 1570  ∃wex 1812  Ⅎwnf 1816   ∈ wcel 2147  ∃*wmo 2565  ∀wral 3080  ∃wrex 3090  ∃*wrmo 3368  Vcvv 3454  {copab 5170  dom cdm 5655   ↾ cres 5657  Fun wfun 6552  ‘cfv 6558

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566

This theorem is used by:  srepdf  36087