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 𝐸 ) ‘ 𝑁 ) )