This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem satfrel

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

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

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑎 = ∅ → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
2 1 releqd ⊢ ( 𝑎 = ∅ → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ↔ Rel ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) )
3 2 imbi2d ⊢ ( 𝑎 = ∅ → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ) ) )
4 fveq2 ⊢ ( 𝑎 = 𝑏 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) )
5 4 releqd ⊢ ( 𝑎 = 𝑏 → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ↔ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) )
6 5 imbi2d ⊢ ( 𝑎 = 𝑏 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) ) )
7 fveq2 ⊢ ( 𝑎 = suc 𝑏 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) )
8 7 releqd ⊢ ( 𝑎 = suc 𝑏 → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ↔ Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) )
9 8 imbi2d ⊢ ( 𝑎 = suc 𝑏 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) ) )
10 fveq2 ⊢ ( 𝑎 = 𝑁 → ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) = ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )
11 10 releqd ⊢ ( 𝑎 = 𝑁 → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ↔ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
12 11 imbi2d ⊢ ( 𝑎 = 𝑁 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑎 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) ) )
13 relopabv ⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) }
14 eqid ⊢ ( 𝑀 Sat 𝐸 ) = ( 𝑀 Sat 𝐸 )
15 14 satfv0 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } )
16 15 releqd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) ↔ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑖 ∈ ω ∃ 𝑗 ∈ ω ( 𝑥 = ( 𝑖 ∈𝑔 𝑗 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ( 𝑎 ‘ 𝑖 ) 𝐸 ( 𝑎 ‘ 𝑗 ) } ) } ) )
17 13 16 mpbiri ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ ∅ ) )
18 pm2.27 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) )
19 simpr ⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) ∧ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) )
20 relopabv ⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) }
21 relun ⊢ ( Rel ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ↔ ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∧ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) )
22 19 20 21 sylanblrc ⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) ∧ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → Rel ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) )
23 14 satfvsuc ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑏 ∈ ω ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) )
24 23 ad4ant123 ⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) ∧ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) = ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) )
25 24 releqd ⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) ∧ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ↔ Rel ( ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( ∃ 𝑣 ∈ ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑎 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑧 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑧 ⟩ } ∪ ( 𝑎 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) ) )
26 22 25 mpbird ⊢ ( ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ 𝑏 ∈ ω ) ∧ Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) )
27 26 exp31 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑏 ∈ ω → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) ) )
28 27 com23 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) → ( 𝑏 ∈ ω → Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) ) )
29 18 28 syld ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → ( 𝑏 ∈ ω → Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) ) )
30 29 com13 ⊢ ( 𝑏 ∈ ω → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑏 ) ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ suc 𝑏 ) ) ) )
31 3 6 9 12 17 30 finds ⊢ ( 𝑁 ∈ ω → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
32 31 com12 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑁 ∈ ω → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) ) )
33 32 3impia ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω ) → Rel ( ( 𝑀 Sat 𝐸 ) ‘ 𝑁 ) )