Metamath Proof Explorer

Theorem srepdflem2

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

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

Proof

Step Hyp Ref Expression
1 srepdflem2.1 ⊢ Ⅎ 𝑓 𝜑
2 srepdflem2.2 ⊢ Ⅎ 𝑤 𝜑
3 srepdflem2.3 ⊢ Ⅎ 𝑦 𝜑
4 srepdflem2.4 ⊢ Ⅎ 𝑧 𝜑
5 srepdflem2.5 ⊢ ( 𝜑 → 𝑥 ∈ 𝑀 )
6 srepdflem2.6 ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
7 srepdflem2.7 ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) )
8 srepdflem2.8 ⊢ 𝐹 = ( 𝐺 ↾ 𝑥 )
9 srepdflem2.9 ⊢ 𝐺 = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) }
10 nfa1 ⊢ Ⅎ 𝑦 ∀ 𝑦 𝜓
11 10 rmo2i ⊢ ( ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) → ∃* 𝑧 ∈ 𝑀 ∀ 𝑦 𝜓 )
12 11 ralimi ⊢ ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) → ∀ 𝑤 ∈ 𝑀 ∃* 𝑧 ∈ 𝑀 ∀ 𝑦 𝜓 )
13 funopab ⊢ ( Fun { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) } ↔ ∀ 𝑤 ∃* 𝑧 ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) )
14 9 funeqi ⊢ ( Fun 𝐺 ↔ Fun { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) } )
15 2reu5lem2 ⊢ ( ∀ 𝑤 ∈ 𝑀 ∃* 𝑧 ∈ 𝑀 ∀ 𝑦 𝜓 ↔ ∀ 𝑤 ∃* 𝑧 ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) )
16 13 14 15 3bitr4i ⊢ ( Fun 𝐺 ↔ ∀ 𝑤 ∈ 𝑀 ∃* 𝑧 ∈ 𝑀 ∀ 𝑦 𝜓 )
17 12 16 sylibr ⊢ ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 𝜓 → 𝑧 = 𝑦 ) → Fun 𝐺 )
18 resfunexg ⊢ ( ( Fun 𝐺 ∧ 𝑥 ∈ V ) → ( 𝐺 ↾ 𝑥 ) ∈ V )
19 18 elvd ⊢ ( Fun 𝐺 → ( 𝐺 ↾ 𝑥 ) ∈ V )
20 7 17 19 3syl ⊢ ( 𝜑 → ( 𝐺 ↾ 𝑥 ) ∈ V )
21 8 20 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ V )
22 elex2 ⊢ ( 𝑥 ∈ 𝑀 → ∃ 𝑦 𝑦 ∈ 𝑀 )
23 rmoeq ⊢ ∃* 𝑧 ∈ 𝑀 𝑧 = ( 𝑓 ‘ 𝑤 )
24 simp3 ⊢ ( ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → ( 𝑓 ‘ 𝑤 ) = 𝑧 )
25 24 eqcomd ⊢ ( ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = ( 𝑓 ‘ 𝑤 ) )
26 25 spsv ⊢ ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = ( 𝑓 ‘ 𝑤 ) )
27 26 rmoimi ⊢ ( ∃* 𝑧 ∈ 𝑀 𝑧 = ( 𝑓 ‘ 𝑤 ) → ∃* 𝑧 ∈ 𝑀 ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) )
28 23 27 ax-mp ⊢ ∃* 𝑧 ∈ 𝑀 ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 )
29 nfa1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 )
30 29 rmo6 ⊢ ( ∃* 𝑧 ∈ 𝑀 ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ↔ ( ∃ 𝑦 𝑦 ∈ 𝑀 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) ) )
31 28 30 mpbi ⊢ ( ∃ 𝑦 𝑦 ∈ 𝑀 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) )
32 5 22 31 3syl ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑀 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) )
34 2 33 ralrimia ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) )
35 34 6 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) )
36 1 35 alrimi ⊢ ( 𝜑 → ∀ 𝑓 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) )
37 nfv ⊢ Ⅎ 𝑦 𝑤 ∈ 𝑀
38 nfv ⊢ Ⅎ 𝑦 𝑧 ∈ 𝑀
39 37 38 10 nf3an ⊢ Ⅎ 𝑦 ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 )
40 39 nfopab ⊢ Ⅎ 𝑦 { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) }
41 9 40 nfcxfr ⊢ Ⅎ 𝑦 𝐺
42 nfcv ⊢ Ⅎ 𝑦 𝑥
43 41 42 nfres ⊢ Ⅎ 𝑦 ( 𝐺 ↾ 𝑥 )
44 8 43 nfcxfr ⊢ Ⅎ 𝑦 𝐹
45 44 nfeq2 ⊢ Ⅎ 𝑦 𝑓 = 𝐹
46 nfopab2 ⊢ Ⅎ 𝑧 { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) }
47 9 46 nfcxfr ⊢ Ⅎ 𝑧 𝐺
48 nfcv ⊢ Ⅎ 𝑧 𝑥
49 47 48 nfres ⊢ Ⅎ 𝑧 ( 𝐺 ↾ 𝑥 )
50 8 49 nfcxfr ⊢ Ⅎ 𝑧 𝐹
51 50 nfeq2 ⊢ Ⅎ 𝑧 𝑓 = 𝐹
52 nfopab1 ⊢ Ⅎ 𝑤 { ⟨ 𝑤 , 𝑧 ⟩ ∣ ( 𝑤 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ∧ ∀ 𝑦 𝜓 ) }
53 9 52 nfcxfr ⊢ Ⅎ 𝑤 𝐺
54 nfcv ⊢ Ⅎ 𝑤 𝑥
55 53 54 nfres ⊢ Ⅎ 𝑤 ( 𝐺 ↾ 𝑥 )
56 8 55 nfcxfr ⊢ Ⅎ 𝑤 𝐹
57 56 nfeq2 ⊢ Ⅎ 𝑤 𝑓 = 𝐹
58 funeq ⊢ ( 𝑓 = 𝐹 → ( Fun 𝑓 ↔ Fun 𝐹 ) )
59 dmeq ⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
60 59 eleq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑤 ∈ dom 𝑓 ↔ 𝑤 ∈ dom 𝐹 ) )
61 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑤 ) )
62 61 eqeq1d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑤 ) = 𝑧 ↔ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) )
63 58 60 62 3anbi123d ⊢ ( 𝑓 = 𝐹 → ( ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ↔ ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) )
64 45 63 albid ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ↔ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) )
65 64 anbi2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ↔ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) )
66 57 65 rexbid ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) )
67 66 bibi2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ↔ ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
68 51 67 ralbid ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ↔ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
69 45 68 rexbid ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ↔ ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
70 69 spcgv ⊢ ( 𝐹 ∈ V → ( ∀ 𝑓 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) ) )
71 21 36 70 sylc ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) )
72 2 7 8 9 srepdflem1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) )
73 biantr ⊢ ( ( ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) ∧ ( ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) ) → ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) )
74 72 73 sylan2 ⊢ ( ( ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) ∧ ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) ) → ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) )
75 74 expcom ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑀 ) → ( ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) → ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) ) )
76 4 75 ralimdaa ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) → ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) ) )
77 76 a1d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑀 → ( ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) → ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) ) ) )
78 3 77 reximdai ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝐹 ∧ 𝑤 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑤 ) = 𝑧 ) ) ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) ) )
79 71 78 mpd ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 𝜓 ) ) )