Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  satfrel Structured version   Visualization version   GIF version

Theorem satfrel 35372
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.)
Assertion
Ref Expression
satfrel ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → Rel ((𝑀 Sat 𝐸)‘𝑁))

Proof of Theorem satfrel
Dummy variables 𝑎 𝑖 𝑗 𝑢 𝑣 𝑥 𝑦 𝑧 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 6906 . . . . . 6 (𝑎 = ∅ → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘∅))
21releqd 5788 . . . . 5 (𝑎 = ∅ → (Rel ((𝑀 Sat 𝐸)‘𝑎) ↔ Rel ((𝑀 Sat 𝐸)‘∅)))
32imbi2d 340 . . . 4 (𝑎 = ∅ → (((𝑀𝑉𝐸𝑊) → Rel ((𝑀 Sat 𝐸)‘𝑎)) ↔ ((𝑀𝑉𝐸𝑊) → Rel ((𝑀 Sat 𝐸)‘∅))))
4 fveq2 6906 . . . . . 6 (𝑎 = 𝑏 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘𝑏))
54releqd 5788 . . . . 5 (𝑎 = 𝑏 → (Rel ((𝑀 Sat 𝐸)‘𝑎) ↔ Rel ((𝑀 Sat 𝐸)‘𝑏)))
65imbi2d 340 . . . 4 (𝑎 = 𝑏 → (((𝑀𝑉𝐸𝑊) → Rel ((𝑀 Sat 𝐸)‘𝑎)) ↔ ((𝑀𝑉𝐸𝑊) → Rel ((𝑀 Sat 𝐸)‘𝑏))))
7 fveq2 6906 . . . . . 6 (𝑎 = suc 𝑏 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘suc 𝑏))
87releqd 5788 . . . . 5 (𝑎 = suc 𝑏 → (Rel ((𝑀 Sat 𝐸)‘𝑎) ↔ Rel ((𝑀 Sat 𝐸)‘suc 𝑏)))
98imbi2d 340 . . . 4 (𝑎 = suc 𝑏 → (((𝑀𝑉𝐸𝑊) → Rel ((𝑀 Sat 𝐸)‘𝑎)) ↔ ((𝑀𝑉𝐸𝑊) → Rel ((𝑀 Sat 𝐸)‘suc 𝑏))))
10 fveq2 6906 . . . . . 6 (𝑎 = 𝑁 → ((𝑀 Sat 𝐸)‘𝑎) = ((𝑀 Sat 𝐸)‘𝑁))
1110releqd 5788 . . . . 5 (𝑎 = 𝑁 → (Rel ((𝑀 Sat 𝐸)‘𝑎) ↔ Rel ((𝑀 Sat 𝐸)‘𝑁)))
1211imbi2d 340 . . . 4 (𝑎 = 𝑁 → (((𝑀𝑉𝐸𝑊) → Rel ((𝑀 Sat 𝐸)‘𝑎)) ↔ ((𝑀𝑉𝐸𝑊) → Rel ((𝑀 Sat 𝐸)‘𝑁))))
13 relopabv 5831 . . . . 5 Rel {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})}
14 eqid 2737 . . . . . . 7 (𝑀 Sat 𝐸) = (𝑀 Sat 𝐸)
1514satfv0 35363 . . . . . 6 ((𝑀𝑉𝐸𝑊) → ((𝑀 Sat 𝐸)‘∅) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})})
1615releqd 5788 . . . . 5 ((𝑀𝑉𝐸𝑊) → (Rel ((𝑀 Sat 𝐸)‘∅) ↔ Rel {⟨𝑥, 𝑦⟩ ∣ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑥 = (𝑖𝑔𝑗) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ (𝑎𝑖)𝐸(𝑎𝑗)})}))
1713, 16mpbiri 258 . . . 4 ((𝑀𝑉𝐸𝑊) → Rel ((𝑀 Sat 𝐸)‘∅))
18 pm2.27 42 . . . . . 6 ((𝑀𝑉𝐸𝑊) → (((𝑀𝑉𝐸𝑊) → Rel ((𝑀 Sat 𝐸)‘𝑏)) → Rel ((𝑀 Sat 𝐸)‘𝑏)))
19 simpr 484 . . . . . . . . . 10 ((((𝑀𝑉𝐸𝑊) ∧ 𝑏 ∈ ω) ∧ Rel ((𝑀 Sat 𝐸)‘𝑏)) → Rel ((𝑀 Sat 𝐸)‘𝑏))
20 relopabv 5831 . . . . . . . . . 10 Rel {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}
21 relun 5821 . . . . . . . . . 10 (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𝑢)}))}))
2219, 20, 21sylanblrc 590 . . . . . . . . 9 ((((𝑀𝑉𝐸𝑊) ∧ 𝑏 ∈ ω) ∧ Rel ((𝑀 Sat 𝐸)‘𝑏)) → Rel (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
2314satfvsuc 35366 . . . . . . . . . . 11 ((𝑀𝑉𝐸𝑊𝑏 ∈ ω) → ((𝑀 Sat 𝐸)‘suc 𝑏) = (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
2423ad4ant123 1173 . . . . . . . . . 10 ((((𝑀𝑉𝐸𝑊) ∧ 𝑏 ∈ ω) ∧ Rel ((𝑀 Sat 𝐸)‘𝑏)) → ((𝑀 Sat 𝐸)‘suc 𝑏) = (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))}))
2524releqd 5788 . . . . . . . . 9 ((((𝑀𝑉𝐸𝑊) ∧ 𝑏 ∈ ω) ∧ Rel ((𝑀 Sat 𝐸)‘𝑏)) → (Rel ((𝑀 Sat 𝐸)‘suc 𝑏) ↔ Rel (((𝑀 Sat 𝐸)‘𝑏) ∪ {⟨𝑥, 𝑦⟩ ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑏)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑏)(𝑥 = ((1st𝑢)⊼𝑔(1st𝑣)) ∧ 𝑦 = ((𝑀m ω) ∖ ((2nd𝑢) ∩ (2nd𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st𝑢) ∧ 𝑦 = {𝑎 ∈ (𝑀m ω) ∣ ∀𝑧𝑀 ({⟨𝑖, 𝑧⟩} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd𝑢)}))})))
2622, 25mpbird 257 . . . . . . . 8 ((((𝑀𝑉𝐸𝑊) ∧ 𝑏 ∈ ω) ∧ Rel ((𝑀 Sat 𝐸)‘𝑏)) → Rel ((𝑀 Sat 𝐸)‘suc 𝑏))
2726exp31 419 . . . . . . 7 ((𝑀𝑉𝐸𝑊) → (𝑏 ∈ ω → (Rel ((𝑀 Sat 𝐸)‘𝑏) → Rel ((𝑀 Sat 𝐸)‘suc 𝑏))))
2827com23 86 . . . . . 6 ((𝑀𝑉𝐸𝑊) → (Rel ((𝑀 Sat 𝐸)‘𝑏) → (𝑏 ∈ ω → Rel ((𝑀 Sat 𝐸)‘suc 𝑏))))
2918, 28syld 47 . . . . 5 ((𝑀𝑉𝐸𝑊) → (((𝑀𝑉𝐸𝑊) → Rel ((𝑀 Sat 𝐸)‘𝑏)) → (𝑏 ∈ ω → Rel ((𝑀 Sat 𝐸)‘suc 𝑏))))
3029com13 88 . . . 4 (𝑏 ∈ ω → (((𝑀𝑉𝐸𝑊) → Rel ((𝑀 Sat 𝐸)‘𝑏)) → ((𝑀𝑉𝐸𝑊) → Rel ((𝑀 Sat 𝐸)‘suc 𝑏))))
313, 6, 9, 12, 17, 30finds 7918 . . 3 (𝑁 ∈ ω → ((𝑀𝑉𝐸𝑊) → Rel ((𝑀 Sat 𝐸)‘𝑁)))
3231com12 32 . 2 ((𝑀𝑉𝐸𝑊) → (𝑁 ∈ ω → Rel ((𝑀 Sat 𝐸)‘𝑁)))
33323impia 1118 1 ((𝑀𝑉𝐸𝑊𝑁 ∈ ω) → Rel ((𝑀 Sat 𝐸)‘𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 848  w3a 1087   = wceq 1540  wcel 2108  wral 3061  wrex 3070  {crab 3436  cdif 3948  cun 3949  cin 3950  c0 4333  {csn 4626  cop 4632   class class class wbr 5143  {copab 5205  cres 5687  Rel wrel 5690  suc csuc 6386  cfv 6561  (class class class)co 7431  ωcom 7887  1st c1st 8012  2nd c2nd 8013  m cmap 8866  𝑔cgoe 35338  𝑔cgna 35339  𝑔cgol 35340   Sat csat 35341
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-goel 35345  df-sat 35348
This theorem is referenced by:  satfdmlem  35373  satffunlem1lem2  35408  satffunlem2lem2  35411
  Copyright terms: Public domain W3C validator