Theorem fwfffunres 35764

Description: If 𝜓 is function-like over 𝐴, then 𝐹 matches its behavior over 𝑥. (Contributed by BTernaryTau, 28-Sep-2026.)

Hypotheses

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

Assertion

Ref	Expression
fwfffunres	⊢ (𝜑 → ((𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥 ∧ 𝜓)) ↔ (𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))

Distinct variable groups:   𝑧,𝑤   𝑦,𝐴,𝑧

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

Proof of Theorem fwfffunres

Step	Hyp	Ref	Expression
1		fwfffunres.1	. . . . . 6 ⊢ Ⅎ𝑦𝜓
2		fwfffunres.2	. . . . . 6 ⊢ (𝜑 → ∀𝑤 ∈ 𝐴 ∃𝑦∀𝑧 ∈ 𝐴 (𝜓 → 𝑧 = 𝑦))
3		eqid 2760	. . . . . 6 ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)}
4	1, 2, 3	fwfffun 35763	. . . . 5 ⊢ (𝜑 → ((𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓) ↔ (𝑤 ∈ dom {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)} ∧ ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)}‘𝑤) = 𝑧)))
5	4	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑥) → ((𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓) ↔ (𝑤 ∈ dom {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)} ∧ ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)}‘𝑤) = 𝑧)))
6		fwfffunres.3	. . . . . . . . . 10 ⊢ 𝐹 = ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)} ↾ 𝑥)
7	6	dmeqi 5885	. . . . . . . . 9 ⊢ dom 𝐹 = dom ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)} ↾ 𝑥)
8		dmres 6002	. . . . . . . . 9 ⊢ dom ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)} ↾ 𝑥) = (𝑥 ∩ dom {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)})
9	7, 8	eqtri 2783	. . . . . . . 8 ⊢ dom 𝐹 = (𝑥 ∩ dom {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)})
10	9	elin2 4100	. . . . . . 7 ⊢ (𝑤 ∈ dom 𝐹 ↔ (𝑤 ∈ 𝑥 ∧ 𝑤 ∈ dom {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)}))
11	10	baib 545	. . . . . 6 ⊢ (𝑤 ∈ 𝑥 → (𝑤 ∈ dom 𝐹 ↔ 𝑤 ∈ dom {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)}))
12	6	fveq1i 6886	. . . . . . . 8 ⊢ (𝐹‘𝑤) = (({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)} ↾ 𝑥)‘𝑤)
13		fvres 6904	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑥 → (({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)} ↾ 𝑥)‘𝑤) = ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)}‘𝑤))
14	12, 13	eqtrid 2807	. . . . . . 7 ⊢ (𝑤 ∈ 𝑥 → (𝐹‘𝑤) = ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)}‘𝑤))
15	14	eqeq1d 2762	. . . . . 6 ⊢ (𝑤 ∈ 𝑥 → ((𝐹‘𝑤) = 𝑧 ↔ ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)}‘𝑤) = 𝑧))
16	11, 15	anbi12d 644	. . . . 5 ⊢ (𝑤 ∈ 𝑥 → ((𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧) ↔ (𝑤 ∈ dom {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)} ∧ ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)}‘𝑤) = 𝑧)))
17	16	adantl 487	. . . 4 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑥) → ((𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧) ↔ (𝑤 ∈ dom {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)} ∧ ({⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)}‘𝑤) = 𝑧)))
18	5, 17	bitr4d 285	. . 3 ⊢ ((𝜑 ∧ 𝑤 ∈ 𝑥) → ((𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓) ↔ (𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
19	18	pm5.32da 590	. 2 ⊢ (𝜑 → ((𝑤 ∈ 𝑥 ∧ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)) ↔ (𝑤 ∈ 𝑥 ∧ (𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧))))
20		an4 669	. . . 4 ⊢ (((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (𝑤 ∈ 𝑥 ∧ 𝜓)) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝐴 ∧ 𝜓)))
21		ancom 466	. . . . 5 ⊢ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) ↔ (𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝐴))
22	21	anbi1i 636	. . . 4 ⊢ (((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝐴 ∧ 𝜓)) ↔ ((𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝐴) ∧ (𝑤 ∈ 𝐴 ∧ 𝜓)))
23		an4 669	. . . 4 ⊢ (((𝑤 ∈ 𝑥 ∧ 𝑧 ∈ 𝐴) ∧ (𝑤 ∈ 𝐴 ∧ 𝜓)) ↔ ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝜓)))
24	20, 22, 23	3bitri 300	. . 3 ⊢ (((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (𝑤 ∈ 𝑥 ∧ 𝜓)) ↔ ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝜓)))
25		13an22anass 1379	. . 3 ⊢ ((𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥 ∧ 𝜓)) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (𝑤 ∈ 𝑥 ∧ 𝜓)))
26		13an22anass 1379	. . 3 ⊢ ((𝑤 ∈ 𝑥 ∧ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)) ↔ ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝜓)))
27	24, 25, 26	3bitr4i 306	. 2 ⊢ ((𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥 ∧ 𝜓)) ↔ (𝑤 ∈ 𝑥 ∧ (𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ∧ 𝜓)))
28	10	simplbi 502	. . . 4 ⊢ (𝑤 ∈ dom 𝐹 → 𝑤 ∈ 𝑥)
29	28	adantr 486	. . 3 ⊢ ((𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧) → 𝑤 ∈ 𝑥)
30	29	pm4.71ri 570	. 2 ⊢ ((𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧) ↔ (𝑤 ∈ 𝑥 ∧ (𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))
31	19, 27, 30	3bitr4g 317	1 ⊢ (𝜑 → ((𝑧 ∈ 𝐴 ∧ (𝑤 ∈ 𝐴 ∧ 𝑤 ∈ 𝑥 ∧ 𝜓)) ↔ (𝑤 ∈ dom 𝐹 ∧ (𝐹‘𝑤) = 𝑧)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569  ∃wex 1811  Ⅎwnf 1815   ∈ wcel 2144  ∀wral 3076   ∩ cin 4089  {copab 5166  dom cdm 5650   ↾ cres 5652  ‘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:  srepdflem1  36004