Metamath Proof Explorer


Theorem satefvfmla1

Description: The simplified satisfaction predicate at two Godel-sets of membership combined with a Godel-set for NAND. (Contributed by AV, 17-Nov-2023)

Ref Expression
Hypothesis satfv1fvfmla1.x X = I 𝑔 J 𝑔 K 𝑔 L
Assertion satefvfmla1 M V I ω J ω K ω L ω M Sat X = a M ω | ¬ a I a J ¬ a K a L

Proof

Step Hyp Ref Expression
1 satfv1fvfmla1.x X = I 𝑔 J 𝑔 K 𝑔 L
2 1 ovexi X V
3 2 jctr M V M V X V
4 3 3ad2ant1 M V I ω J ω K ω L ω M V X V
5 satefv M V X V M Sat X = M Sat E M × M ω X
6 4 5 syl M V I ω J ω K ω L ω M Sat X = M Sat E M × M ω X
7 sqxpexg M V M × M V
8 inex2g M × M V E M × M V
9 7 8 syl M V E M × M V
10 9 ancli M V M V E M × M V
11 10 3ad2ant1 M V I ω J ω K ω L ω M V E M × M V
12 satom M V E M × M V M Sat E M × M ω = i ω M Sat E M × M i
13 11 12 syl M V I ω J ω K ω L ω M Sat E M × M ω = i ω M Sat E M × M i
14 13 fveq1d M V I ω J ω K ω L ω M Sat E M × M ω X = i ω M Sat E M × M i X
15 satfun M V E M × M V M Sat E M × M ω : Fmla ω 𝒫 M ω
16 11 15 syl M V I ω J ω K ω L ω M Sat E M × M ω : Fmla ω 𝒫 M ω
17 16 ffund M V I ω J ω K ω L ω Fun M Sat E M × M ω
18 13 eqcomd M V I ω J ω K ω L ω i ω M Sat E M × M i = M Sat E M × M ω
19 18 funeqd M V I ω J ω K ω L ω Fun i ω M Sat E M × M i Fun M Sat E M × M ω
20 17 19 mpbird M V I ω J ω K ω L ω Fun i ω M Sat E M × M i
21 1onn 1 𝑜 ω
22 21 a1i M V I ω J ω K ω L ω 1 𝑜 ω
23 1 2goelgoanfmla1 I ω J ω K ω L ω X Fmla 1 𝑜
24 23 3adant1 M V I ω J ω K ω L ω X Fmla 1 𝑜
25 21 a1i M V 1 𝑜 ω
26 satfdmfmla M V E M × M V 1 𝑜 ω dom M Sat E M × M 1 𝑜 = Fmla 1 𝑜
27 9 25 26 mpd3an23 M V dom M Sat E M × M 1 𝑜 = Fmla 1 𝑜
28 27 3ad2ant1 M V I ω J ω K ω L ω dom M Sat E M × M 1 𝑜 = Fmla 1 𝑜
29 24 28 eleqtrrd M V I ω J ω K ω L ω X dom M Sat E M × M 1 𝑜
30 eqid i ω M Sat E M × M i = i ω M Sat E M × M i
31 30 fviunfun Fun i ω M Sat E M × M i 1 𝑜 ω X dom M Sat E M × M 1 𝑜 i ω M Sat E M × M i X = M Sat E M × M 1 𝑜 X
32 20 22 29 31 syl3anc M V I ω J ω K ω L ω i ω M Sat E M × M i X = M Sat E M × M 1 𝑜 X
33 14 32 eqtrd M V I ω J ω K ω L ω M Sat E M × M ω X = M Sat E M × M 1 𝑜 X
34 1 satfv1fvfmla1 M V E M × M V I ω J ω K ω L ω M Sat E M × M 1 𝑜 X = a M ω | ¬ a I E M × M a J ¬ a K E M × M a L
35 10 34 syl3an1 M V I ω J ω K ω L ω M Sat E M × M 1 𝑜 X = a M ω | ¬ a I E M × M a J ¬ a K E M × M a L
36 brin a I E M × M a J a I E a J a I M × M a J
37 elmapi a M ω a : ω M
38 ffvelrn a : ω M I ω a I M
39 38 ex a : ω M I ω a I M
40 37 39 syl a M ω I ω a I M
41 ffvelrn a : ω M J ω a J M
42 41 ex a : ω M J ω a J M
43 37 42 syl a M ω J ω a J M
44 40 43 anim12d a M ω I ω J ω a I M a J M
45 44 com12 I ω J ω a M ω a I M a J M
46 45 3ad2ant2 M V I ω J ω K ω L ω a M ω a I M a J M
47 46 imp M V I ω J ω K ω L ω a M ω a I M a J M
48 brxp a I M × M a J a I M a J M
49 47 48 sylibr M V I ω J ω K ω L ω a M ω a I M × M a J
50 49 biantrud M V I ω J ω K ω L ω a M ω a I E a J a I E a J a I M × M a J
51 fvex a J V
52 51 epeli a I E a J a I a J
53 50 52 bitr3di M V I ω J ω K ω L ω a M ω a I E a J a I M × M a J a I a J
54 36 53 syl5bb M V I ω J ω K ω L ω a M ω a I E M × M a J a I a J
55 54 notbid M V I ω J ω K ω L ω a M ω ¬ a I E M × M a J ¬ a I a J
56 brin a K E M × M a L a K E a L a K M × M a L
57 ffvelrn a : ω M K ω a K M
58 57 ex a : ω M K ω a K M
59 37 58 syl a M ω K ω a K M
60 ffvelrn a : ω M L ω a L M
61 60 ex a : ω M L ω a L M
62 37 61 syl a M ω L ω a L M
63 59 62 anim12d a M ω K ω L ω a K M a L M
64 63 com12 K ω L ω a M ω a K M a L M
65 64 3ad2ant3 M V I ω J ω K ω L ω a M ω a K M a L M
66 65 imp M V I ω J ω K ω L ω a M ω a K M a L M
67 brxp a K M × M a L a K M a L M
68 66 67 sylibr M V I ω J ω K ω L ω a M ω a K M × M a L
69 68 biantrud M V I ω J ω K ω L ω a M ω a K E a L a K E a L a K M × M a L
70 fvex a L V
71 70 epeli a K E a L a K a L
72 69 71 bitr3di M V I ω J ω K ω L ω a M ω a K E a L a K M × M a L a K a L
73 56 72 syl5bb M V I ω J ω K ω L ω a M ω a K E M × M a L a K a L
74 73 notbid M V I ω J ω K ω L ω a M ω ¬ a K E M × M a L ¬ a K a L
75 55 74 orbi12d M V I ω J ω K ω L ω a M ω ¬ a I E M × M a J ¬ a K E M × M a L ¬ a I a J ¬ a K a L
76 75 rabbidva M V I ω J ω K ω L ω a M ω | ¬ a I E M × M a J ¬ a K E M × M a L = a M ω | ¬ a I a J ¬ a K a L
77 35 76 eqtrd M V I ω J ω K ω L ω M Sat E M × M 1 𝑜 X = a M ω | ¬ a I a J ¬ a K a L
78 6 33 77 3eqtrd M V I ω J ω K ω L ω M Sat X = a M ω | ¬ a I a J ¬ a K a L