Metamath Proof Explorer

Theorem satfsschain

Description: The binary relation of a satisfaction predicate as function over wff codes is an increasing chain (with respect to inclusion). (Contributed by AV, 15-Oct-2023)

Ref Expression
Hypothesis satfsschain.s ⊢ 𝑆 = ( 𝑀 Sat 𝐸 )
Assertion satfsschain ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐵 ⊆ 𝐴 → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 satfsschain.s ⊢ 𝑆 = ( 𝑀 Sat 𝐸 )
2 fveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝑆 ‘ 𝑏 ) = ( 𝑆 ‘ 𝐵 ) )
3 2 sseq2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑏 ) ↔ ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝐵 ) ) )
4 3 imbi2d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑏 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝐵 ) ) ) )
5 fveq2 ⊢ ( 𝑏 = 𝑎 → ( 𝑆 ‘ 𝑏 ) = ( 𝑆 ‘ 𝑎 ) )
6 5 sseq2d ⊢ ( 𝑏 = 𝑎 → ( ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑏 ) ↔ ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑎 ) ) )
7 6 imbi2d ⊢ ( 𝑏 = 𝑎 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑏 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑎 ) ) ) )
8 fveq2 ⊢ ( 𝑏 = suc 𝑎 → ( 𝑆 ‘ 𝑏 ) = ( 𝑆 ‘ suc 𝑎 ) )
9 8 sseq2d ⊢ ( 𝑏 = suc 𝑎 → ( ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑏 ) ↔ ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ suc 𝑎 ) ) )
10 9 imbi2d ⊢ ( 𝑏 = suc 𝑎 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑏 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ suc 𝑎 ) ) ) )
11 fveq2 ⊢ ( 𝑏 = 𝐴 → ( 𝑆 ‘ 𝑏 ) = ( 𝑆 ‘ 𝐴 ) )
12 11 sseq2d ⊢ ( 𝑏 = 𝐴 → ( ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑏 ) ↔ ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝐴 ) ) )
13 12 imbi2d ⊢ ( 𝑏 = 𝐴 → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑏 ) ) ↔ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝐴 ) ) ) )
14 ssidd ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝐵 ) )
15 14 a1i ⊢ ( 𝐵 ∈ ω → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝐵 ) ) )
16 pm2.27 ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑎 ) ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑎 ) ) )
17 16 adantl ⊢ ( ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑎 ) ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑎 ) ) )
18 simpr ⊢ ( ( ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑎 ) ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑎 ) )
19 ssun1 ⊢ ( 𝑆 ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ 𝑎 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑎 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑎 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑧 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑧 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } )
20 simpl ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 𝑀 ∈ 𝑉 )
21 simpr ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 𝐸 ∈ 𝑊 )
22 simplll ⊢ ( ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → 𝑎 ∈ ω )
23 1 satfvsuc ⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑎 ∈ ω ) → ( 𝑆 ‘ suc 𝑎 ) = ( ( 𝑆 ‘ 𝑎 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑎 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑎 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑧 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑧 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) )
24 20 21 22 23 syl2an23an ⊢ ( ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( 𝑆 ‘ suc 𝑎 ) = ( ( 𝑆 ‘ 𝑎 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑎 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑎 ) ( 𝑥 = ( ( 1st ‘ 𝑢 ) ⊼𝑔 ( 1st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑m ω ) ∖ ( ( 2nd ‘ 𝑢 ) ∩ ( 2nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀𝑔 𝑖 ( 1st ‘ 𝑢 ) ∧ 𝑦 = { 𝑧 ∈ ( 𝑀 ↑m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑧 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2nd ‘ 𝑢 ) } ) ) } ) )
25 19 24 sseqtrrid ⊢ ( ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( 𝑆 ‘ 𝑎 ) ⊆ ( 𝑆 ‘ suc 𝑎 ) )
26 25 adantr ⊢ ( ( ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑎 ) ) → ( 𝑆 ‘ 𝑎 ) ⊆ ( 𝑆 ‘ suc 𝑎 ) )
27 18 26 sstrd ⊢ ( ( ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) ∧ ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑎 ) ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ suc 𝑎 ) )
28 27 ex ⊢ ( ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑎 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ suc 𝑎 ) ) )
29 17 28 syld ⊢ ( ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑎 ) ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ suc 𝑎 ) ) )
30 29 ex ⊢ ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑎 ) ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ suc 𝑎 ) ) ) )
31 30 com23 ⊢ ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) → ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝑎 ) ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ suc 𝑎 ) ) ) )
32 4 7 10 13 15 31 findsg ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝐴 ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝐴 ) ) )
33 32 ex ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 ⊆ 𝐴 → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝐴 ) ) ) )
34 33 com23 ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → ( 𝐵 ⊆ 𝐴 → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝐴 ) ) ) )
35 34 impcom ⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐵 ⊆ 𝐴 → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝐴 ) ) )