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 S = M Sat E
Assertion satfsschain M V E W A ω B ω B A S B S A

Proof

Step Hyp Ref Expression
1 satfsschain.s S = M Sat E
2 fveq2 b = B S b = S B
3 2 sseq2d b = B S B S b S B S B
4 3 imbi2d b = B M V E W S B S b M V E W S B S B
5 fveq2 b = a S b = S a
6 5 sseq2d b = a S B S b S B S a
7 6 imbi2d b = a M V E W S B S b M V E W S B S a
8 fveq2 b = suc a S b = S suc a
9 8 sseq2d b = suc a S B S b S B S suc a
10 9 imbi2d b = suc a M V E W S B S b M V E W S B S suc a
11 fveq2 b = A S b = S A
12 11 sseq2d b = A S B S b S B S A
13 12 imbi2d b = A M V E W S B S b M V E W S B S A
14 ssidd M V E W S B S B
15 14 a1i B ω M V E W S B S B
16 pm2.27 M V E W M V E W S B S a S B S a
17 16 adantl a ω B ω B a M V E W M V E W S B S a S B S a
18 simpr a ω B ω B a M V E W S B S a S B S a
19 ssun1 S a S a x y | u S a v S a x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = z M ω | k M i k z ω i 2 nd u
20 simpl M V E W M V
21 simpr M V E W E W
22 simplll a ω B ω B a M V E W a ω
23 1 satfvsuc M V E W a ω S suc a = S a x y | u S a v S a x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = z M ω | k M i k z ω i 2 nd u
24 20 21 22 23 syl2an23an a ω B ω B a M V E W S suc a = S a x y | u S a v S a x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = z M ω | k M i k z ω i 2 nd u
25 19 24 sseqtrrid a ω B ω B a M V E W S a S suc a
26 25 adantr a ω B ω B a M V E W S B S a S a S suc a
27 18 26 sstrd a ω B ω B a M V E W S B S a S B S suc a
28 27 ex a ω B ω B a M V E W S B S a S B S suc a
29 17 28 syld a ω B ω B a M V E W M V E W S B S a S B S suc a
30 29 ex a ω B ω B a M V E W M V E W S B S a S B S suc a
31 30 com23 a ω B ω B a M V E W S B S a M V E W S B S suc a
32 4 7 10 13 15 31 findsg A ω B ω B A M V E W S B S A
33 32 ex A ω B ω B A M V E W S B S A
34 33 com23 A ω B ω M V E W B A S B S A
35 34 impcom M V E W A ω B ω B A S B S A