Theorem srepdflem1 36085

Description: Lemma for srepdf 36087. (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 1949	. . 3 ⊢ Ⅎ𝑤 𝑧 ∈ 𝑀
3	1, 2	nfan 1934	. 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 2191	. . . . . . . . . 10 ⊢ Ⅎ𝑦∀𝑦𝜓
10		srepdflem1.2	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
11		rexex 3096	. . . . . . . . . . . 12 ⊢ (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∃𝑦∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
12	11	ralimi 3103	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∀𝑤 ∈ 𝑀 ∃𝑦∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
13	10, 12	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ 𝑀 ∃𝑦∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦))
14		srepdflem1.3	. . . . . . . . . . 11 ⊢ 𝐹 = (𝐺 ↾ 𝑥)
15		srepdflem1.4	. . . . . . . . . . . 12 ⊢ 𝐺 = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}
16	15	reseq1i 5977	. . . . . . . . . . 11 ⊢ (𝐺 ↾ 𝑥) = ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)} ↾ 𝑥)
17	14, 16	eqtri 2786	. . . . . . . . . 10 ⊢ 𝐹 = ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)} ↾ 𝑥)
18	9, 13, 17	fwfffunres 35788	. . . . . . . . 9 ⊢ (𝜑 → ((𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)) ↔ (𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
19	9	rmo2i 3839	. . . . . . . . . . . . . 14 ⊢ (∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓)
20	19	ralimi 3103	. . . . . . . . . . . . 13 ⊢ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → ∀𝑤 ∈ 𝑀 ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓)
21		funopab 6595	. . . . . . . . . . . . . 14 ⊢ (Fun {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)} ↔ ∀𝑤∃*𝑧(𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓))
22	15	funeqi 6580	. . . . . . . . . . . . . 14 ⊢ (Fun 𝐺 ↔ Fun {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)})
23		2reu5lem2 3717	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑀 ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓 ↔ ∀𝑤∃*𝑧(𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓))
24	21, 22, 23	3bitr4i 306	. . . . . . . . . . . . 13 ⊢ (Fun 𝐺 ↔ ∀𝑤 ∈ 𝑀 ∃*𝑧 ∈ 𝑀 ∀𝑦𝜓)
25	20, 24	sylibr 237	. . . . . . . . . . . 12 ⊢ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜓 → 𝑧 = 𝑦) → Fun 𝐺)
26		funres 6602	. . . . . . . . . . . 12 ⊢ (Fun 𝐺 → Fun (𝐺 ↾ 𝑥))
27	10, 25, 26	3syl 19	. . . . . . . . . . 11 ⊢ (𝜑 → Fun (𝐺 ↾ 𝑥))
28	14	funeqi 6580	. . . . . . . . . . 11 ⊢ (Fun 𝐹 ↔ Fun (𝐺 ↾ 𝑥))
29	27, 28	sylibr 237	. . . . . . . . . 10 ⊢ (𝜑 → Fun 𝐹)
30	29	3biant1d 1510	. . . . . . . . 9 ⊢ (𝜑 → ((𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧) ↔ (Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
31	18, 30	bitrd 282	. . . . . . . 8 ⊢ (𝜑 → ((𝑧 ∈ 𝑀 ∧ (𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓)) ↔ (Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
32	8, 31	sylan9bbr 520	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → ((𝑤 ∈ 𝑀 ∧ 𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) ↔ (Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
33		nfv 1949	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑤 ∈ 𝑀
34		nfv 1949	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦 𝑧 ∈ 𝑀
35	33, 34, 9	nf3an 1936	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦(𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)
36	35	nfopab 5177	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦{⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀𝑦𝜓)}
37	15, 36	nfcxfr 2924	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦𝐺
38		nfcv 2926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑦𝑥
39	37, 38	nfres 5983	. . . . . . . . . . 11 ⊢ Ⅎ𝑦(𝐺 ↾ 𝑥)
40	14, 39	nfcxfr 2924	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐹
41	40	nffun 6582	. . . . . . . . 9 ⊢ Ⅎ𝑦Fun 𝐹
42	40	nfdm 5940	. . . . . . . . . 10 ⊢ Ⅎ𝑦dom 𝐹
43	42	nfcri 2918	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑤 ∈ dom 𝐹
44		nfcv 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑤
45	40, 44	nffv 6918	. . . . . . . . . 10 ⊢ Ⅎ𝑦(𝐹‘𝑤)
46	45	nfeq1 2941	. . . . . . . . 9 ⊢ Ⅎ𝑦(𝐹‘𝑤) = 𝑧
47	41, 43, 46	nf3an 1936	. . . . . . . 8 ⊢ Ⅎ𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)
48	47	19.3 2242	. . . . . . 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 3278	1 ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑀) → (∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜓) ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))))

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  {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-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-rab 3417  df-v 3456  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-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-res 5667  df-iota 6512  df-fun 6560  df-fn 6561  df-fv 6566

This theorem is used by:  srepdflem2  36086