Metamath Proof Explorer

Theorem satfv0fun

Description: The value of the satisfaction predicate as function over wff codes at (/) is a function. (Contributed by AV, 15-Oct-2023)

Ref Expression
Assertion satfv0fun ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )

Proof

Step Hyp Ref Expression
1 funopab ⊢ ( Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) } ↔ ∀ 𝑥 ∃* 𝑦 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) )
2 oveq1 ⊢ ( 𝑖 = 𝑘 → ( 𝑖 ∈𝑔 𝑗 ) = ( 𝑘 ∈𝑔 𝑗 ) )
3 2 eqeq2d ⊢ ( 𝑖 = 𝑘 → ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ↔ 𝑥 = ( 𝑘 ∈𝑔 𝑗 ) ) )
4 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝑓 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑘 ) )
5 4 breq1d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) ↔ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑗 ) ) )
6 5 rabbidv ⊢ ( 𝑖 = 𝑘 → { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } )
7 6 eqeq2d ⊢ ( 𝑖 = 𝑘 → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ↔ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) )
8 3 7 anbi12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ↔ ( 𝑥 = ( 𝑘 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ) )
9 oveq2 ⊢ ( 𝑗 = 𝑙 → ( 𝑘 ∈𝑔 𝑗 ) = ( 𝑘 ∈𝑔 𝑙 ) )
10 9 eqeq2d ⊢ ( 𝑗 = 𝑙 → ( 𝑥 = ( 𝑘 ∈𝑔 𝑗 ) ↔ 𝑥 = ( 𝑘 ∈𝑔 𝑙 ) ) )
11 fveq2 ⊢ ( 𝑗 = 𝑙 → ( 𝑓 ‘ 𝑗 ) = ( 𝑓 ‘ 𝑙 ) )
12 11 breq2d ⊢ ( 𝑗 = 𝑙 → ( ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑗 ) ↔ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) ) )
13 12 rabbidv ⊢ ( 𝑗 = 𝑙 → { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } )
14 13 eqeq2d ⊢ ( 𝑗 = 𝑙 → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ↔ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } ) )
15 10 14 anbi12d ⊢ ( 𝑗 = 𝑙 → ( ( 𝑥 = ( 𝑘 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ↔ ( 𝑥 = ( 𝑘 ∈𝑔 𝑙 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } ) ) )
16 8 15 cbvrex2vw ⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ↔ ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( 𝑘 ∈𝑔 𝑙 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } ) )
17 eqtr2 ⊢ ( ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑥 = ( 𝑘 ∈𝑔 𝑙 ) ) → ( 𝑖 ∈𝑔 𝑗 ) = ( 𝑘 ∈𝑔 𝑙 ) )
18 goeleq12bg ⊢ ( ( ( 𝑘 ∈ ω ∧ 𝑙 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( ( 𝑖 ∈𝑔 𝑗 ) = ( 𝑘 ∈𝑔 𝑙 ) ↔ ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) ) )
19 4 adantr ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → ( 𝑓 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑘 ) )
20 19 eqcomd ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑖 ) )
21 11 adantl ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑓 ‘ 𝑙 ) )
22 21 eqcomd ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → ( 𝑓 ‘ 𝑙 ) = ( 𝑓 ‘ 𝑗 ) )
23 20 22 breq12d ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → ( ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) ↔ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) ) )
24 23 rabbidv ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } )
25 eqeq12 ⊢ ( ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) → ( 𝑦 = 𝑧 ↔ { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) )
26 24 25 syl5ibrcom ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → ( ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) → 𝑦 = 𝑧 ) )
27 26 expd ⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑙 ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } → 𝑦 = 𝑧 ) ) )
28 18 27 syl6bi ⊢ ( ( ( 𝑘 ∈ ω ∧ 𝑙 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( ( 𝑖 ∈𝑔 𝑗 ) = ( 𝑘 ∈𝑔 𝑙 ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } → 𝑦 = 𝑧 ) ) ) )
29 17 28 syl5 ⊢ ( ( ( 𝑘 ∈ ω ∧ 𝑙 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑥 = ( 𝑘 ∈𝑔 𝑙 ) ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } → 𝑦 = 𝑧 ) ) ) )
30 29 expd ⊢ ( ( ( 𝑘 ∈ ω ∧ 𝑙 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) → ( 𝑥 = ( 𝑘 ∈𝑔 𝑙 ) → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } → 𝑦 = 𝑧 ) ) ) ) )
31 30 imp4a ⊢ ( ( ( 𝑘 ∈ ω ∧ 𝑙 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) → ( ( 𝑥 = ( 𝑘 ∈𝑔 𝑙 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } ) → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } → 𝑦 = 𝑧 ) ) ) )
32 31 com34 ⊢ ( ( ( 𝑘 ∈ ω ∧ 𝑙 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) → ( 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } → ( ( 𝑥 = ( 𝑘 ∈𝑔 𝑙 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } ) → 𝑦 = 𝑧 ) ) ) )
33 32 impd ⊢ ( ( ( 𝑘 ∈ ω ∧ 𝑙 ∈ ω ) ∧ ( 𝑖 ∈ ω ∧ 𝑗 ∈ ω ) ) → ( ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) → ( ( 𝑥 = ( 𝑘 ∈𝑔 𝑙 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } ) → 𝑦 = 𝑧 ) ) )
34 33 rexlimdvva ⊢ ( ( 𝑘 ∈ ω ∧ 𝑙 ∈ ω ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) → ( ( 𝑥 = ( 𝑘 ∈𝑔 𝑙 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } ) → 𝑦 = 𝑧 ) ) )
35 34 com23 ⊢ ( ( 𝑘 ∈ ω ∧ 𝑙 ∈ ω ) → ( ( 𝑥 = ( 𝑘 ∈𝑔 𝑙 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) → 𝑦 = 𝑧 ) ) )
36 35 rexlimivv ⊢ ( ∃ 𝑘 ∈ ω ∃ 𝑙 ∈ ω ( 𝑥 = ( 𝑘 ∈𝑔 𝑙 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑘 ) 𝐸 ( 𝑓 ‘ 𝑙 ) } ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) → 𝑦 = 𝑧 ) )
37 16 36 sylbi ⊢ ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) → 𝑦 = 𝑧 ) )
38 37 imp ⊢ ( ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ) → 𝑦 = 𝑧 )
39 38 gen2 ⊢ ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ) → 𝑦 = 𝑧 )
40 eqeq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ↔ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) )
41 40 anbi2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ↔ ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ) )
42 41 2rexbidv ⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ↔ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ) )
43 42 mo4 ⊢ ( ∃* 𝑦 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ↔ ∀ 𝑦 ∀ 𝑧 ( ( ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ∧ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑧 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) ) → 𝑦 = 𝑧 ) )
44 39 43 mpbir ⊢ ∃* 𝑦 ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } )
45 1 44 mpgbir ⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) }
46 eqid ⊢ ( 𝑀 Sat 𝐸 ) = ( 𝑀 Sat 𝐸 )
47 46 satfv0 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) } )
48 47 funeqd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ↔ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑓 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑓 ‘ 𝑖 ) 𝐸 ( 𝑓 ‘ 𝑗 ) } ) } ) )
49 45 48 mpbiri ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )