Metamath Proof Explorer

Theorem srepdf

Description: Derive the strong version of the Axiom Scheme of Replacement used in wfaxrep (see comments there) from a particular instance of that version of Replacement. Note that this theorem depends on ax-rep , so it does not follow that we could replace ax-rep with an axiom that lacks a wff metavariable. (Contributed by BTernaryTau, 30-Sep-2026)

Ref Expression
Hypotheses srepdf.1 ⊢ Ⅎ 𝑓 𝜑
srepdf.2 ⊢ Ⅎ 𝑤 𝜑
srepdf.3 ⊢ Ⅎ 𝑥 𝜑
srepdf.4 ⊢ Ⅎ 𝑦 𝜑
srepdf.5 ⊢ Ⅎ 𝑧 𝜑
srepdf.6 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
Assertion srepdf ( 𝜑 → ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) ) )

Proof

Step Hyp Ref Expression
1 srepdf.1 ⊢ Ⅎ 𝑓 𝜑
2 srepdf.2 ⊢ Ⅎ 𝑤 𝜑
3 srepdf.3 ⊢ Ⅎ 𝑥 𝜑
4 srepdf.4 ⊢ Ⅎ 𝑦 𝜑
5 srepdf.5 ⊢ Ⅎ 𝑧 𝜑
6 srepdf.6 ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
7 ax-5 ⊢ ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) → ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) )
8 nfv ⊢ Ⅎ 𝑔 ( 𝜑 ∧ 𝑥 ∈ 𝑀 )
9 nfa1 ⊢ Ⅎ 𝑔 ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 )
10 8 9 nfan ⊢ Ⅎ 𝑔 ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) )
11 nfv ⊢ Ⅎ 𝑤 𝑥 ∈ 𝑀
12 2 11 nfan ⊢ Ⅎ 𝑤 ( 𝜑 ∧ 𝑥 ∈ 𝑀 )
13 nfra1 ⊢ Ⅎ 𝑤 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 )
14 13 nfal ⊢ Ⅎ 𝑤 ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 )
15 12 14 nfan ⊢ Ⅎ 𝑤 ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) )
16 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝑀
17 4 16 nfan ⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ 𝑀 )
18 nfcv ⊢ Ⅎ 𝑦 𝑀
19 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 )
20 18 19 nfralw ⊢ Ⅎ 𝑦 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 )
21 20 nfal ⊢ Ⅎ 𝑦 ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 )
22 17 21 nfan ⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) )
23 nfv ⊢ Ⅎ 𝑧 𝑥 ∈ 𝑀
24 5 23 nfan ⊢ Ⅎ 𝑧 ( 𝜑 ∧ 𝑥 ∈ 𝑀 )
25 nfcv ⊢ Ⅎ 𝑧 𝑀
26 nfra1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 )
27 25 26 nfrexw ⊢ Ⅎ 𝑧 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 )
28 25 27 nfralw ⊢ Ⅎ 𝑧 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 )
29 28 nfal ⊢ Ⅎ 𝑧 ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 )
30 24 29 nfan ⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) )
31 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) ) → 𝑥 ∈ 𝑀 )
32 1 6 alrimi ⊢ ( 𝜑 → ∀ 𝑓 ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
33 funeq ⊢ ( 𝑓 = 𝑔 → ( Fun 𝑓 ↔ Fun 𝑔 ) )
34 dmeq ⊢ ( 𝑓 = 𝑔 → dom 𝑓 = dom 𝑔 )
35 34 eleq2d ⊢ ( 𝑓 = 𝑔 → ( 𝑤 ∈ dom 𝑓 ↔ 𝑤 ∈ dom 𝑔 ) )
36 fveq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ 𝑤 ) = ( 𝑔 ‘ 𝑤 ) )
37 36 eqeq1d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ‘ 𝑤 ) = 𝑧 ↔ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) )
38 33 35 37 3anbi123d ⊢ ( 𝑓 = 𝑔 → ( ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ↔ ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) ) )
39 38 albidv ⊢ ( 𝑓 = 𝑔 → ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ↔ ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) ) )
40 39 imbi1d ⊢ ( 𝑓 = 𝑔 → ( ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) ↔ ( ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) ) )
41 40 rexralbidv ⊢ ( 𝑓 = 𝑔 → ( ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) ↔ ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) ) )
42 41 ralbidv ⊢ ( 𝑓 = 𝑔 → ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) ↔ ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) ) )
43 39 anbi2d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ↔ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) ) ) )
44 43 rexbidv ⊢ ( 𝑓 = 𝑔 → ( ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) ) ) )
45 44 bibi2d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ↔ ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
46 45 rexralbidv ⊢ ( 𝑓 = 𝑔 → ( ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ↔ ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
47 42 46 imbi12d ⊢ ( 𝑓 = 𝑔 → ( ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) ↔ ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) ) ) ) ) )
48 47 ralbidv ⊢ ( 𝑓 = 𝑔 → ( ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) ) ) ) ) )
49 48 cbvalvw ⊢ ( ∀ 𝑓 ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) ↔ ∀ 𝑔 ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
50 32 49 sylib ⊢ ( 𝜑 → ∀ 𝑔 ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
51 50 19.21bi ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
52 51 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
53 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) ) → ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑔 ∧ 𝑤 ∈ dom 𝑔 ∧ ( 𝑔 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
54 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) ) → ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) )
55 54 19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) ) → ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) )
56 eqid ⊢ ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) } ↾ 𝑥 ) = ( { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) } ↾ 𝑥 )
57 eqid ⊢ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) }
58 10 15 22 30 31 53 55 56 57 srepdflem2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) ∧ ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) )
59 58 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( ∀ 𝑔 ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) ) )
60 7 59 syl5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑀 ) → ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) ) )
61 3 60 ralrimia ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) ) )