Theorem srepdflem1 36004

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

Hypotheses

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

Assertion

Ref	Expression
srepdflem1	⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → (∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))))

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

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

Proof of Theorem srepdflem1

Step	Hyp	Ref	Expression
1		srepdflem1.1	. . 3 ⊢ Ⅎ𝑤𝜑
2		nfv 1946	. . 3 ⊢ Ⅎ𝑤 𝑧 ∈ 𝑀
3	1, 2	nfan 1931	. 2 ⊢ Ⅎ𝑤(𝜑 ∧ 𝑧 ∈ 𝑀)
4		3anass 1111	. . . 4 ⊢ ((𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) ↔ (𝑤 ∈ 𝑀 ∧ (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)))
5	4	baibr 546	. . 3 ⊢ (𝑤 ∈ 𝑀 → ((𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) ↔ (𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)))
6		simp2 1155	. . . . . 6 ⊢ ((𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) → 𝑤 ∈ 𝑥)
7	6	a1i 11	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → ((𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) → 𝑤 ∈ 𝑥))
8		ibar 538	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑀 → ((𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) ↔ (𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓))))
9		nfa1 2187	. . . . . . . . . 10 ⊢ Ⅎ𝑦∀𝑦𝜓
10		srepdflem1.2	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
11		rexex 3092	. . . . . . . . . . . 12 ⊢ (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∃𝑦∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
12	11	ralimi 3099	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∀𝑤 ∈ 𝑀 ∃𝑦∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
13	10, 12	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ 𝑀 ∃𝑦∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
14		srepdflem1.3	. . . . . . . . . . 11 ⊢ 𝐹 = (𝐺 ↾ 𝑥)
15		srepdflem1.4	. . . . . . . . . . . 12 ⊢ 𝐺 = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}
16	15	reseq1i 5965	. . . . . . . . . . 11 ⊢ (𝐺 ↾ 𝑥) = ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)} ↾ 𝑥)
17	14, 16	eqtri 2783	. . . . . . . . . 10 ⊢ 𝐹 = ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)} ↾ 𝑥)
18	9, 13, 17	fwfffunres 35764	. . . . . . . . 9 ⊢ (𝜑 → ((𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)) ↔ (𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
19	9	rmo2i 3834	. . . . . . . . . . . . . 14 ⊢ (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓)
20	19	ralimi 3099	. . . . . . . . . . . . 13 ⊢ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∀𝑤 ∈ 𝑀 ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓)
21		funopab 6575	. . . . . . . . . . . . . 14 ⊢ (Fun {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)} ↔ ∀𝑤∃*𝑧(𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓))
22	15	funeqi 6560	. . . . . . . . . . . . . 14 ⊢ (Fun 𝐺 ↔ Fun {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)})
23		2reu5lem2 3713	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑀 ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓 ↔ ∀𝑤∃*𝑧(𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓))
24	21, 22, 23	3bitr4i 306	. . . . . . . . . . . . 13 ⊢ (Fun 𝐺 ↔ ∀𝑤 ∈ 𝑀 ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓)
25	20, 24	sylibr 237	. . . . . . . . . . . 12 ⊢ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → Fun 𝐺)
26		funres 6582	. . . . . . . . . . . 12 ⊢ (Fun 𝐺 → Fun (𝐺 ↾ 𝑥))
27	10, 25, 26	3syl 19	. . . . . . . . . . 11 ⊢ (𝜑 → Fun (𝐺 ↾ 𝑥))
28	14	funeqi 6560	. . . . . . . . . . 11 ⊢ (Fun 𝐹 ↔ Fun (𝐺 ↾ 𝑥))
29	27, 28	sylibr 237	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝐹)
30	29	3biant1d 1509	. . . . . . . . 9 ⊢ (𝜑 → ((𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧) ↔ (Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
31	18, 30	bitrd 282	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)) ↔ (Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
32	8, 31	sylan9bbr 520	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → ((𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) ↔ (Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
33		nfv 1946	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑤 ∈ 𝑀
34		nfv 1946	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑧 ∈ 𝑀
35	33, 34, 9	nf3an 1933	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)
36	35	nfopab 5173	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦{⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}
37	15, 36	nfcxfr 2920	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦𝐺
38		nfcv 2922	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦𝑥
39	37, 38	nfres 5971	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝐺 ↾ 𝑥)
40	14, 39	nfcxfr 2920	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐹
41	40	nffun 6562	. . . . . . . . 9 ⊢ Ⅎ𝑦Fun 𝐹
42	40	nfdm 5932	. . . . . . . . . 10 ⊢ Ⅎ𝑦dom 𝐹
43	42	nfcri 2914	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑤 ∈ dom 𝐹
44		nfcv 2922	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑤
45	40, 44	nffv 6895	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝐹‘𝑤)
46	45	nfeq1 2937	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝐹‘𝑤) = 𝑧
47	41, 43, 46	nf3an 1933	. . . . . . . 8 ⊢ Ⅎ𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)
48	47	19.3 2238	. . . . . . 7 ⊢ (∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧) ↔ (Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))
49	32, 48	bitr4di 292	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → ((𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) ↔ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
50	49	biimpd 232	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → ((𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) → ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
51	7, 50	jcad 522	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → ((𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) → (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))))
52	49	biimprd 251	. . . . 5 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → (∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧) → (𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)))
53	52	adantld 496	. . . 4 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → ((𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)) → (𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)))
54	51, 53	impbid 215	. . 3 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → ((𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) ↔ (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))))
55	5, 54	sylan9bbr 520	. 2 ⊢ (((𝜑 ∧ 𝑧 ∈ 𝑀) ∧ 𝑤 ∈ 𝑀) → ((𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) ↔ (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))))
56	3, 55	rexbida 3274	1 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → (∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))))

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  {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-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-rab 3413  df-v 3452  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-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-res 5662  df-iota 6494  df-fun 6540  df-fn 6541  df-fv 6546

This theorem is used by:  srepdflem2  36005