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

Theorem satefvfmla1 32667
 Description: The simplified satisfaction predicate at two Godel-sets of membership combined with a Godel-set for NAND. (Contributed by AV, 17-Nov-2023.)
Hypothesis
Ref Expression
satfv1fvfmla1.x 𝑋 = ((𝐼𝑔𝐽)⊼𝑔(𝐾𝑔𝐿))
Assertion
Ref Expression
satefvfmla1 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (𝑀 Sat 𝑋) = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝐼) ∈ (𝑎𝐽) ∨ ¬ (𝑎𝐾) ∈ (𝑎𝐿))})
Distinct variable groups:   𝐼,𝑎   𝐽,𝑎   𝐾,𝑎   𝐿,𝑎   𝑀,𝑎   𝑉,𝑎
Allowed substitution hint:   𝑋(𝑎)

Proof of Theorem satefvfmla1
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 satfv1fvfmla1.x . . . . . 6 𝑋 = ((𝐼𝑔𝐽)⊼𝑔(𝐾𝑔𝐿))
21ovexi 7184 . . . . 5 𝑋 ∈ V
32jctr 527 . . . 4 (𝑀𝑉 → (𝑀𝑉𝑋 ∈ V))
433ad2ant1 1129 . . 3 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (𝑀𝑉𝑋 ∈ V))
5 satefv 32656 . . 3 ((𝑀𝑉𝑋 ∈ V) → (𝑀 Sat 𝑋) = (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω)‘𝑋))
64, 5syl 17 . 2 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (𝑀 Sat 𝑋) = (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω)‘𝑋))
7 sqxpexg 7471 . . . . . . . 8 (𝑀𝑉 → (𝑀 × 𝑀) ∈ V)
8 inex2g 5217 . . . . . . . 8 ((𝑀 × 𝑀) ∈ V → ( E ∩ (𝑀 × 𝑀)) ∈ V)
97, 8syl 17 . . . . . . 7 (𝑀𝑉 → ( E ∩ (𝑀 × 𝑀)) ∈ V)
109ancli 551 . . . . . 6 (𝑀𝑉 → (𝑀𝑉 ∧ ( E ∩ (𝑀 × 𝑀)) ∈ V))
11103ad2ant1 1129 . . . . 5 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (𝑀𝑉 ∧ ( E ∩ (𝑀 × 𝑀)) ∈ V))
12 satom 32598 . . . . 5 ((𝑀𝑉 ∧ ( E ∩ (𝑀 × 𝑀)) ∈ V) → ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω) = 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖))
1311, 12syl 17 . . . 4 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω) = 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖))
1413fveq1d 6667 . . 3 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω)‘𝑋) = ( 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖)‘𝑋))
15 satfun 32653 . . . . . . 7 ((𝑀𝑉 ∧ ( E ∩ (𝑀 × 𝑀)) ∈ V) → ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω):(Fmla‘ω)⟶𝒫 (𝑀m ω))
1611, 15syl 17 . . . . . 6 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω):(Fmla‘ω)⟶𝒫 (𝑀m ω))
1716ffund 6513 . . . . 5 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → Fun ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω))
1813eqcomd 2827 . . . . . 6 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖) = ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω))
1918funeqd 6372 . . . . 5 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (Fun 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖) ↔ Fun ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω)))
2017, 19mpbird 259 . . . 4 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → Fun 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖))
21 1onn 8259 . . . . 5 1o ∈ ω
2221a1i 11 . . . 4 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 1o ∈ ω)
2312goelgoanfmla1 32666 . . . . . 6 (((𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝑋 ∈ (Fmla‘1o))
24233adant1 1126 . . . . 5 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝑋 ∈ (Fmla‘1o))
2521a1i 11 . . . . . . 7 (𝑀𝑉 → 1o ∈ ω)
26 satfdmfmla 32642 . . . . . . 7 ((𝑀𝑉 ∧ ( E ∩ (𝑀 × 𝑀)) ∈ V ∧ 1o ∈ ω) → dom ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘1o) = (Fmla‘1o))
279, 25, 26mpd3an23 1459 . . . . . 6 (𝑀𝑉 → dom ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘1o) = (Fmla‘1o))
28273ad2ant1 1129 . . . . 5 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → dom ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘1o) = (Fmla‘1o))
2924, 28eleqtrrd 2916 . . . 4 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → 𝑋 ∈ dom ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘1o))
30 eqid 2821 . . . . 5 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖) = 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖)
3130fviunfun 7640 . . . 4 ((Fun 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖) ∧ 1o ∈ ω ∧ 𝑋 ∈ dom ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘1o)) → ( 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖)‘𝑋) = (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘1o)‘𝑋))
3220, 22, 29, 31syl3anc 1367 . . 3 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → ( 𝑖 ∈ ω ((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘𝑖)‘𝑋) = (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘1o)‘𝑋))
3314, 32eqtrd 2856 . 2 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘ω)‘𝑋) = (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘1o)‘𝑋))
341satfv1fvfmla1 32665 . . . 4 (((𝑀𝑉 ∧ ( E ∩ (𝑀 × 𝑀)) ∈ V) ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘1o)‘𝑋) = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝐼)( E ∩ (𝑀 × 𝑀))(𝑎𝐽) ∨ ¬ (𝑎𝐾)( E ∩ (𝑀 × 𝑀))(𝑎𝐿))})
3510, 34syl3an1 1159 . . 3 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘1o)‘𝑋) = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝐼)( E ∩ (𝑀 × 𝑀))(𝑎𝐽) ∨ ¬ (𝑎𝐾)( E ∩ (𝑀 × 𝑀))(𝑎𝐿))})
36 brin 5111 . . . . . . 7 ((𝑎𝐼)( E ∩ (𝑀 × 𝑀))(𝑎𝐽) ↔ ((𝑎𝐼) E (𝑎𝐽) ∧ (𝑎𝐼)(𝑀 × 𝑀)(𝑎𝐽)))
37 fvex 6678 . . . . . . . . 9 (𝑎𝐽) ∈ V
3837epeli 5463 . . . . . . . 8 ((𝑎𝐼) E (𝑎𝐽) ↔ (𝑎𝐼) ∈ (𝑎𝐽))
39 elmapi 8422 . . . . . . . . . . . . . . 15 (𝑎 ∈ (𝑀m ω) → 𝑎:ω⟶𝑀)
40 ffvelrn 6844 . . . . . . . . . . . . . . . 16 ((𝑎:ω⟶𝑀𝐼 ∈ ω) → (𝑎𝐼) ∈ 𝑀)
4140ex 415 . . . . . . . . . . . . . . 15 (𝑎:ω⟶𝑀 → (𝐼 ∈ ω → (𝑎𝐼) ∈ 𝑀))
4239, 41syl 17 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝑀m ω) → (𝐼 ∈ ω → (𝑎𝐼) ∈ 𝑀))
43 ffvelrn 6844 . . . . . . . . . . . . . . . 16 ((𝑎:ω⟶𝑀𝐽 ∈ ω) → (𝑎𝐽) ∈ 𝑀)
4443ex 415 . . . . . . . . . . . . . . 15 (𝑎:ω⟶𝑀 → (𝐽 ∈ ω → (𝑎𝐽) ∈ 𝑀))
4539, 44syl 17 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝑀m ω) → (𝐽 ∈ ω → (𝑎𝐽) ∈ 𝑀))
4642, 45anim12d 610 . . . . . . . . . . . . 13 (𝑎 ∈ (𝑀m ω) → ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → ((𝑎𝐼) ∈ 𝑀 ∧ (𝑎𝐽) ∈ 𝑀)))
4746com12 32 . . . . . . . . . . . 12 ((𝐼 ∈ ω ∧ 𝐽 ∈ ω) → (𝑎 ∈ (𝑀m ω) → ((𝑎𝐼) ∈ 𝑀 ∧ (𝑎𝐽) ∈ 𝑀)))
48473ad2ant2 1130 . . . . . . . . . . 11 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (𝑎 ∈ (𝑀m ω) → ((𝑎𝐼) ∈ 𝑀 ∧ (𝑎𝐽) ∈ 𝑀)))
4948imp 409 . . . . . . . . . 10 (((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) ∧ 𝑎 ∈ (𝑀m ω)) → ((𝑎𝐼) ∈ 𝑀 ∧ (𝑎𝐽) ∈ 𝑀))
50 brxp 5596 . . . . . . . . . 10 ((𝑎𝐼)(𝑀 × 𝑀)(𝑎𝐽) ↔ ((𝑎𝐼) ∈ 𝑀 ∧ (𝑎𝐽) ∈ 𝑀))
5149, 50sylibr 236 . . . . . . . . 9 (((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) ∧ 𝑎 ∈ (𝑀m ω)) → (𝑎𝐼)(𝑀 × 𝑀)(𝑎𝐽))
5251biantrud 534 . . . . . . . 8 (((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) ∧ 𝑎 ∈ (𝑀m ω)) → ((𝑎𝐼) E (𝑎𝐽) ↔ ((𝑎𝐼) E (𝑎𝐽) ∧ (𝑎𝐼)(𝑀 × 𝑀)(𝑎𝐽))))
5338, 52syl5rbbr 288 . . . . . . 7 (((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) ∧ 𝑎 ∈ (𝑀m ω)) → (((𝑎𝐼) E (𝑎𝐽) ∧ (𝑎𝐼)(𝑀 × 𝑀)(𝑎𝐽)) ↔ (𝑎𝐼) ∈ (𝑎𝐽)))
5436, 53syl5bb 285 . . . . . 6 (((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) ∧ 𝑎 ∈ (𝑀m ω)) → ((𝑎𝐼)( E ∩ (𝑀 × 𝑀))(𝑎𝐽) ↔ (𝑎𝐼) ∈ (𝑎𝐽)))
5554notbid 320 . . . . 5 (((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) ∧ 𝑎 ∈ (𝑀m ω)) → (¬ (𝑎𝐼)( E ∩ (𝑀 × 𝑀))(𝑎𝐽) ↔ ¬ (𝑎𝐼) ∈ (𝑎𝐽)))
56 brin 5111 . . . . . . 7 ((𝑎𝐾)( E ∩ (𝑀 × 𝑀))(𝑎𝐿) ↔ ((𝑎𝐾) E (𝑎𝐿) ∧ (𝑎𝐾)(𝑀 × 𝑀)(𝑎𝐿)))
57 fvex 6678 . . . . . . . . 9 (𝑎𝐿) ∈ V
5857epeli 5463 . . . . . . . 8 ((𝑎𝐾) E (𝑎𝐿) ↔ (𝑎𝐾) ∈ (𝑎𝐿))
59 ffvelrn 6844 . . . . . . . . . . . . . . . 16 ((𝑎:ω⟶𝑀𝐾 ∈ ω) → (𝑎𝐾) ∈ 𝑀)
6059ex 415 . . . . . . . . . . . . . . 15 (𝑎:ω⟶𝑀 → (𝐾 ∈ ω → (𝑎𝐾) ∈ 𝑀))
6139, 60syl 17 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝑀m ω) → (𝐾 ∈ ω → (𝑎𝐾) ∈ 𝑀))
62 ffvelrn 6844 . . . . . . . . . . . . . . . 16 ((𝑎:ω⟶𝑀𝐿 ∈ ω) → (𝑎𝐿) ∈ 𝑀)
6362ex 415 . . . . . . . . . . . . . . 15 (𝑎:ω⟶𝑀 → (𝐿 ∈ ω → (𝑎𝐿) ∈ 𝑀))
6439, 63syl 17 . . . . . . . . . . . . . 14 (𝑎 ∈ (𝑀m ω) → (𝐿 ∈ ω → (𝑎𝐿) ∈ 𝑀))
6561, 64anim12d 610 . . . . . . . . . . . . 13 (𝑎 ∈ (𝑀m ω) → ((𝐾 ∈ ω ∧ 𝐿 ∈ ω) → ((𝑎𝐾) ∈ 𝑀 ∧ (𝑎𝐿) ∈ 𝑀)))
6665com12 32 . . . . . . . . . . . 12 ((𝐾 ∈ ω ∧ 𝐿 ∈ ω) → (𝑎 ∈ (𝑀m ω) → ((𝑎𝐾) ∈ 𝑀 ∧ (𝑎𝐿) ∈ 𝑀)))
67663ad2ant3 1131 . . . . . . . . . . 11 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (𝑎 ∈ (𝑀m ω) → ((𝑎𝐾) ∈ 𝑀 ∧ (𝑎𝐿) ∈ 𝑀)))
6867imp 409 . . . . . . . . . 10 (((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) ∧ 𝑎 ∈ (𝑀m ω)) → ((𝑎𝐾) ∈ 𝑀 ∧ (𝑎𝐿) ∈ 𝑀))
69 brxp 5596 . . . . . . . . . 10 ((𝑎𝐾)(𝑀 × 𝑀)(𝑎𝐿) ↔ ((𝑎𝐾) ∈ 𝑀 ∧ (𝑎𝐿) ∈ 𝑀))
7068, 69sylibr 236 . . . . . . . . 9 (((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) ∧ 𝑎 ∈ (𝑀m ω)) → (𝑎𝐾)(𝑀 × 𝑀)(𝑎𝐿))
7170biantrud 534 . . . . . . . 8 (((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) ∧ 𝑎 ∈ (𝑀m ω)) → ((𝑎𝐾) E (𝑎𝐿) ↔ ((𝑎𝐾) E (𝑎𝐿) ∧ (𝑎𝐾)(𝑀 × 𝑀)(𝑎𝐿))))
7258, 71syl5rbbr 288 . . . . . . 7 (((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) ∧ 𝑎 ∈ (𝑀m ω)) → (((𝑎𝐾) E (𝑎𝐿) ∧ (𝑎𝐾)(𝑀 × 𝑀)(𝑎𝐿)) ↔ (𝑎𝐾) ∈ (𝑎𝐿)))
7356, 72syl5bb 285 . . . . . 6 (((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) ∧ 𝑎 ∈ (𝑀m ω)) → ((𝑎𝐾)( E ∩ (𝑀 × 𝑀))(𝑎𝐿) ↔ (𝑎𝐾) ∈ (𝑎𝐿)))
7473notbid 320 . . . . 5 (((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) ∧ 𝑎 ∈ (𝑀m ω)) → (¬ (𝑎𝐾)( E ∩ (𝑀 × 𝑀))(𝑎𝐿) ↔ ¬ (𝑎𝐾) ∈ (𝑎𝐿)))
7555, 74orbi12d 915 . . . 4 (((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) ∧ 𝑎 ∈ (𝑀m ω)) → ((¬ (𝑎𝐼)( E ∩ (𝑀 × 𝑀))(𝑎𝐽) ∨ ¬ (𝑎𝐾)( E ∩ (𝑀 × 𝑀))(𝑎𝐿)) ↔ (¬ (𝑎𝐼) ∈ (𝑎𝐽) ∨ ¬ (𝑎𝐾) ∈ (𝑎𝐿))))
7675rabbidva 3479 . . 3 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝐼)( E ∩ (𝑀 × 𝑀))(𝑎𝐽) ∨ ¬ (𝑎𝐾)( E ∩ (𝑀 × 𝑀))(𝑎𝐿))} = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝐼) ∈ (𝑎𝐽) ∨ ¬ (𝑎𝐾) ∈ (𝑎𝐿))})
7735, 76eqtrd 2856 . 2 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (((𝑀 Sat ( E ∩ (𝑀 × 𝑀)))‘1o)‘𝑋) = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝐼) ∈ (𝑎𝐽) ∨ ¬ (𝑎𝐾) ∈ (𝑎𝐿))})
786, 33, 773eqtrd 2860 1 ((𝑀𝑉 ∧ (𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ (𝐾 ∈ ω ∧ 𝐿 ∈ ω)) → (𝑀 Sat 𝑋) = {𝑎 ∈ (𝑀m ω) ∣ (¬ (𝑎𝐼) ∈ (𝑎𝐽) ∨ ¬ (𝑎𝐾) ∈ (𝑎𝐿))})
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  {crab 3142  Vcvv 3495   ∩ cin 3935  𝒫 cpw 4539  ∪ ciun 4912   class class class wbr 5059   E cep 5459   × cxp 5548  dom cdm 5550  Fun wfun 6344  ⟶wf 6346  ‘cfv 6350  (class class class)co 7150  ωcom 7574  1oc1o 8089   ↑m cmap 8400  ∈𝑔cgoe 32575  ⊼𝑔cgna 32576   Sat csat 32578  Fmlacfmla 32579   Sat∈ csate 32580 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-inf2 9098  ax-ac2 9879 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ifp 1058  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-int 4870  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-se 5510  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-isom 6359  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-er 8283  df-map 8402  df-en 8504  df-dom 8505  df-sdom 8506  df-card 9362  df-ac 9536  df-goel 32582  df-gona 32583  df-goal 32584  df-sat 32585  df-sate 32586  df-fmla 32587 This theorem is referenced by:  elnanelprv  32671
 Copyright terms: Public domain W3C validator