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