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	⊢ ( 𝑆 ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ 𝑎 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑎 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑎 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑧 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑧 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } )
20		simpl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 𝑀 ∈ 𝑉 )
21		simpr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) → 𝐸 ∈ 𝑊 )
22		simplll	⊢ ( ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → 𝑎 ∈ ω )
23	1	satfvsuc	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑎 ∈ ω ) → ( 𝑆 ‘ suc 𝑎 ) = ( ( 𝑆 ‘ 𝑎 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑎 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑎 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑧 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑧 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
24	20 21 22 23	syl2an23an	⊢ ( ( ( ( 𝑎 ∈ ω ∧ 𝐵 ∈ ω ) ∧ 𝐵 ⊆ 𝑎 ) ∧ ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ) → ( 𝑆 ‘ suc 𝑎 ) = ( ( 𝑆 ‘ 𝑎 ) ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ ( 𝑆 ‘ 𝑎 ) ( ∃ 𝑣 ∈ ( 𝑆 ‘ 𝑎 ) ( 𝑥 = ( ( 1^st ‘ 𝑢 ) ⊼_𝑔 ( 1^st ‘ 𝑣 ) ) ∧ 𝑦 = ( ( 𝑀 ↑_m ω ) ∖ ( ( 2^nd ‘ 𝑢 ) ∩ ( 2^nd ‘ 𝑣 ) ) ) ) ∨ ∃ 𝑖 ∈ ω ( 𝑥 = ∀_𝑔 𝑖 ( 1^st ‘ 𝑢 ) ∧ 𝑦 = { 𝑧 ∈ ( 𝑀 ↑_m ω ) ∣ ∀ 𝑘 ∈ 𝑀 ( { ⟨ 𝑖 , 𝑘 ⟩ } ∪ ( 𝑧 ↾ ( ω ∖ { 𝑖 } ) ) ) ∈ ( 2^nd ‘ 𝑢 ) } ) ) } ) )
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	⊢ ( ( ( 𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐵 ⊆ 𝐴 → ( 𝑆 ‘ 𝐵 ) ⊆ ( 𝑆 ‘ 𝐴 ) ) )

Metamath Proof Explorer

Theorem satfsschain

Proof