Theorem satfsschain 35332

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.)

Hypothesis

Ref	Expression
satfsschain.s	⊢ 𝑆 = (𝑀 Sat 𝐸)

Assertion

Ref	Expression
satfsschain	⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐴 ∈ ω ∧ 𝐵 ∈ ω)) → (𝐵 ⊆ 𝐴 → (𝑆‘𝐵) ⊆ (𝑆‘𝐴)))

Proof of Theorem satfsschain

Dummy variables 𝑎 𝑏 𝑖 𝑘 𝑢 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 846   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ∃wrex 3076  {crab 3443   ∖ cdif 3973   ∪ cun 3974   ∩ cin 3975   ⊆ wss 3976  {csn 4648  ⟨cop 4654  {copab 5228   ↾ cres 5702  suc csuc 6397  ‘cfv 6573  (class class class)co 7448  ωcom 7903  1^st c1st 8028  2^nd c2nd 8029   ↑_m cmap 8884  ⊼_𝑔cgna 35302  ∀_𝑔cgol 35303   Sat csat 35304

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-inf2 9710

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-om 7904  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-rdg 8466  df-sat 35311

This theorem is referenced by:  satfvsucsuc  35333  satffunlem2lem2  35374  satffunlem2  35376  satfun  35379