Metamath Proof Explorer

Theorem satffun

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

Ref Expression
Assertion satffun ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 satfv0fun ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
2 1 3adant3 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
3 fveq2 ⊢ ( 𝑁 = ∅ → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
4 3 funeqd ⊢ ( 𝑁 = ∅ → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ↔ Fun ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) )
5 2 4 syl5ibr ⊢ ( 𝑁 = ∅ → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
6 df-ne ⊢ ( 𝑁 ≠ ∅ ↔ ¬ 𝑁 = ∅ )
7 nnsuc ⊢ ( ( 𝑁 ∈ ω ∧ 𝑁 ≠ ∅ ) → ∃ 𝑛 ∈ ω 𝑁 = suc 𝑛 )
8 suceq ⊢ ( 𝑥 = ∅ → suc 𝑥 = suc ∅ )
9 8 fveq2d ⊢ ( 𝑥 = ∅ → ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑥 ) = ( ( 𝑀 Sat 𝐸 ) ‘ suc ∅ ) )
10 9 funeqd ⊢ ( 𝑥 = ∅ → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑥 ) ↔ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc ∅ ) ) )
11 10 imbi2d ⊢ ( 𝑥 = ∅ → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑥 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc ∅ ) ) ) )
12 suceq ⊢ ( 𝑥 = 𝑦 → suc 𝑥 = suc 𝑦 )
13 12 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑥 ) = ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) )
14 13 funeqd ⊢ ( 𝑥 = 𝑦 → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑥 ) ↔ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) ) )
15 14 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑥 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) ) ) )
16 suceq ⊢ ( 𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦 )
17 16 fveq2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑥 ) = ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑦 ) )
18 17 funeqd ⊢ ( 𝑥 = suc 𝑦 → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑥 ) ↔ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑦 ) ) )
19 18 imbi2d ⊢ ( 𝑥 = suc 𝑦 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑥 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑦 ) ) ) )
20 suceq ⊢ ( 𝑥 = 𝑛 → suc 𝑥 = suc 𝑛 )
21 20 fveq2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑥 ) = ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑛 ) )
22 21 funeqd ⊢ ( 𝑥 = 𝑛 → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑥 ) ↔ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑛 ) ) )
23 22 imbi2d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑥 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑛 ) ) ) )
24 satffunlem1 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc ∅ ) )
25 pm2.27 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) ) )
26 satffunlem2 ⊢ ( ( 𝑦 ∈ ω ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑦 ) ) )
27 26 expcom ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑦 ∈ ω → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑦 ) ) ) )
28 27 com23 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) → ( 𝑦 ∈ ω → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑦 ) ) ) )
29 25 28 syld ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) ) → ( 𝑦 ∈ ω → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑦 ) ) ) )
30 29 com13 ⊢ ( 𝑦 ∈ ω → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑦 ) ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc suc 𝑦 ) ) ) )
31 11 15 19 23 24 30 finds ⊢ ( 𝑛 ∈ ω → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑛 ) ) )
32 31 adantr ⊢ ( ( 𝑛 ∈ ω ∧ 𝑁 = suc 𝑛 ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑛 ) ) )
33 fveq2 ⊢ ( 𝑁 = suc 𝑛 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) = ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑛 ) )
34 33 funeqd ⊢ ( 𝑁 = suc 𝑛 → ( Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ↔ Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑛 ) ) )
35 34 imbi2d ⊢ ( 𝑁 = suc 𝑛 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑛 ) ) ) )
36 35 adantl ⊢ ( ( 𝑛 ∈ ω ∧ 𝑁 = suc 𝑛 ) → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑛 ) ) ) )
37 32 36 mpbird ⊢ ( ( 𝑛 ∈ ω ∧ 𝑁 = suc 𝑛 ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
38 37 rexlimiva ⊢ ( ∃ 𝑛 ∈ ω 𝑁 = suc 𝑛 → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
39 7 38 syl ⊢ ( ( 𝑁 ∈ ω ∧ 𝑁 ≠ ∅ ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
40 39 expcom ⊢ ( 𝑁 ≠ ∅ → ( 𝑁 ∈ ω → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) )
41 6 40 sylbir ⊢ ( ¬ 𝑁 = ∅ → ( 𝑁 ∈ ω → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) )
42 41 com13 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑁 ∈ ω → ( ¬ 𝑁 = ∅ → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) )
43 42 3impia ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → ( ¬ 𝑁 = ∅ → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
44 43 com12 ⊢ ( ¬ 𝑁 = ∅ → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
45 5 44 pm2.61i ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → Fun ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )