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 e.g J ) |g ( K e.g L ) )
Assertion satefvfmla1 
|- ( ( M e. V /\ ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> ( M SatE X ) = { a e. ( M ^m _om ) | ( -. ( a ` I ) e. ( a ` J ) \/ -. ( a ` K ) e. ( a ` L ) ) } )

Proof

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