Theorem srepdflem1

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

	Ref	Expression
Hypotheses	srepdflem1.1	⊢ Ⅎ 𝑤 𝜑
	srepdflem1.2	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) )
	srepdflem1.3	⊢ 𝐹 = ( 𝐺 ↾ 𝑥 )
	srepdflem1.4	⊢ 𝐺 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) }
Assertion	srepdflem1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		srepdflem1.1	⊢ Ⅎ 𝑤 𝜑
2		srepdflem1.2	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) )
3		srepdflem1.3	⊢ 𝐹 = ( 𝐺 ↾ 𝑥 )
4		srepdflem1.4	⊢ 𝐺 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) }
5		nfv	⊢ Ⅎ 𝑤 𝑧 ∈ 𝑀
6	1 5	nfan	⊢ Ⅎ 𝑤 ( 𝜑 ∧ 𝑧 ∈ 𝑀 )
7		3anass	⊢ ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ↔ ( 𝑤 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) )
8	7	baibr	⊢ ( 𝑤 ∈ 𝑀 → ( ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ↔ ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) )
9		simp2	⊢ ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) → 𝑤 ∈ 𝑥 )
10	9	a1i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) → 𝑤 ∈ 𝑥 ) )
11		ibar	⊢ ( 𝑧 ∈ 𝑀 → ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ↔ ( 𝑧 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) ) )
12		nfa1	⊢ Ⅎ 𝑦 ∀ 𝑦 𝜓
13		rexex	⊢ ( ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) )
14	13	ralimi	⊢ ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) → ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) )
15	2 14	syl	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) )
16	4	reseq1i	⊢ ( 𝐺 ↾ 𝑥 ) = ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) } ↾ 𝑥 )
17	3 16	eqtri	⊢ 𝐹 = ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) } ↾ 𝑥 )
18	12 15 17	fwfffunres	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) ↔ ( 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) )
19	12	rmo2i	⊢ ( ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) → ∃* 𝑧 ∈ 𝑀 ∀ 𝑦 𝜓 )
20	19	ralimi	⊢ ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) → ∀ 𝑤 ∈ 𝑀 ∃* 𝑧 ∈ 𝑀 ∀ 𝑦 𝜓 )
21		funopab	⊢ ( Fun { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) } ↔ ∀ 𝑤 ∃* 𝑧 ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) )
22	4	funeqi	⊢ ( Fun 𝐺 ↔ Fun { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) } )
23		2reu5lem2	⊢ ( ∀ 𝑤 ∈ 𝑀 ∃* 𝑧 ∈ 𝑀 ∀ 𝑦 𝜓 ↔ ∀ 𝑤 ∃* 𝑧 ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) )
24	21 22 23	3bitr4i	⊢ ( Fun 𝐺 ↔ ∀ 𝑤 ∈ 𝑀 ∃* 𝑧 ∈ 𝑀 ∀ 𝑦 𝜓 )
25	20 24	sylibr	⊢ ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) → Fun 𝐺 )
26		funres	⊢ ( Fun 𝐺 → Fun ( 𝐺 ↾ 𝑥 ) )
27	2 25 26	3syl	⊢ ( 𝜑 → Fun ( 𝐺 ↾ 𝑥 ) )
28	3	funeqi	⊢ ( Fun 𝐹 ↔ Fun ( 𝐺 ↾ 𝑥 ) )
29	27 28	sylibr	⊢ ( 𝜑 → Fun 𝐹 )
30	29	3biant1d	⊢ ( 𝜑 → ( ( 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ↔ ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) )
31	18 30	bitrd	⊢ ( 𝜑 → ( ( 𝑧 ∈ 𝑀 ∧ ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) ↔ ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) )
32	11 31	sylan9bbr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ↔ ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) )
33		nfv	⊢ Ⅎ 𝑦 𝑤 ∈ 𝑀
34		nfv	⊢ Ⅎ 𝑦 𝑧 ∈ 𝑀
35	33 34 12	nf3an	⊢ Ⅎ 𝑦 ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 )
36	35	nfopab	⊢ Ⅎ 𝑦 { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) }
37	4 36	nfcxfr	⊢ Ⅎ 𝑦 𝐺
38		nfcv	⊢ Ⅎ 𝑦 𝑥
39	37 38	nfres	⊢ Ⅎ 𝑦 ( 𝐺 ↾ 𝑥 )
40	3 39	nfcxfr	⊢ Ⅎ 𝑦 𝐹
41	40	nffun	⊢ Ⅎ 𝑦 Fun 𝐹
42	40	nfdm	⊢ Ⅎ 𝑦 dom 𝐹
43	42	nfcri	⊢ Ⅎ 𝑦 𝑤 ∈ dom 𝐹
44		nfcv	⊢ Ⅎ 𝑦 𝑤
45	40 44	nffv	⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑤 )
46	45	nfeq1	⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑤 ) = 𝑧
47	41 43 46	nf3an	⊢ Ⅎ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 )
48	47	19.3	⊢ ( ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ↔ ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) )
49	32 48	bitr4di	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ↔ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) )
50	49	biimpd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) → ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) )
51	10 50	jcad	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) → ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) )
52	49	biimprd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) → ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) )
53	52	adantld	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) → ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) )
54	51 53	impbid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( ( 𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ↔ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) )
55	8 54	sylan9bbr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) ∧ 𝑤 ∈ 𝑀 ) → ( ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ↔ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) )
56	6 55	rexbida	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) )