Metamath Proof Explorer


Theorem satefvfmla0

Description: The simplified satisfaction predicate for wff codes of height 0. (Contributed by AV, 4-Nov-2023)

Ref Expression
Assertion satefvfmla0
|- ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( M SatE X ) = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) e. ( a ` ( 2nd ` ( 2nd ` X ) ) ) } )

Proof

Step Hyp Ref Expression
1 satefv
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( M SatE X ) = ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` X ) )
2 incom
 |-  ( _E i^i ( M X. M ) ) = ( ( M X. M ) i^i _E )
3 sqxpexg
 |-  ( M e. V -> ( M X. M ) e. _V )
4 inex1g
 |-  ( ( M X. M ) e. _V -> ( ( M X. M ) i^i _E ) e. _V )
5 3 4 syl
 |-  ( M e. V -> ( ( M X. M ) i^i _E ) e. _V )
6 2 5 eqeltrid
 |-  ( M e. V -> ( _E i^i ( M X. M ) ) e. _V )
7 6 ancli
 |-  ( M e. V -> ( M e. V /\ ( _E i^i ( M X. M ) ) e. _V ) )
8 7 adantr
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( M e. V /\ ( _E i^i ( M X. M ) ) e. _V ) )
9 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 ) )
10 8 9 syl
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) = U_ i e. _om ( ( M Sat ( _E i^i ( M X. M ) ) ) ` i ) )
11 10 fveq1d
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` X ) = ( U_ i e. _om ( ( M Sat ( _E i^i ( M X. M ) ) ) ` i ) ` X ) )
12 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 ) )
13 8 12 syl
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) : ( Fmla ` _om ) --> ~P ( M ^m _om ) )
14 13 ffund
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> Fun ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) )
15 10 eqcomd
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> U_ i e. _om ( ( M Sat ( _E i^i ( M X. M ) ) ) ` i ) = ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) )
16 15 funeqd
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( Fun U_ i e. _om ( ( M Sat ( _E i^i ( M X. M ) ) ) ` i ) <-> Fun ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ) )
17 14 16 mpbird
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> Fun U_ i e. _om ( ( M Sat ( _E i^i ( M X. M ) ) ) ` i ) )
18 peano1
 |-  (/) e. _om
19 18 a1i
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> (/) e. _om )
20 18 a1i
 |-  ( M e. V -> (/) e. _om )
21 satfdmfmla
 |-  ( ( M e. V /\ ( _E i^i ( M X. M ) ) e. _V /\ (/) e. _om ) -> dom ( ( M Sat ( _E i^i ( M X. M ) ) ) ` (/) ) = ( Fmla ` (/) ) )
22 6 20 21 mpd3an23
 |-  ( M e. V -> dom ( ( M Sat ( _E i^i ( M X. M ) ) ) ` (/) ) = ( Fmla ` (/) ) )
23 22 eqcomd
 |-  ( M e. V -> ( Fmla ` (/) ) = dom ( ( M Sat ( _E i^i ( M X. M ) ) ) ` (/) ) )
24 23 eleq2d
 |-  ( M e. V -> ( X e. ( Fmla ` (/) ) <-> X e. dom ( ( M Sat ( _E i^i ( M X. M ) ) ) ` (/) ) ) )
25 24 biimpa
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> X e. dom ( ( M Sat ( _E i^i ( M X. M ) ) ) ` (/) ) )
26 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 )
27 26 fviunfun
 |-  ( ( Fun U_ i e. _om ( ( M Sat ( _E i^i ( M X. M ) ) ) ` i ) /\ (/) e. _om /\ X e. dom ( ( M Sat ( _E i^i ( M X. M ) ) ) ` (/) ) ) -> ( U_ i e. _om ( ( M Sat ( _E i^i ( M X. M ) ) ) ` i ) ` X ) = ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` (/) ) ` X ) )
28 17 19 25 27 syl3anc
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( U_ i e. _om ( ( M Sat ( _E i^i ( M X. M ) ) ) ` i ) ` X ) = ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` (/) ) ` X ) )
29 11 28 eqtrd
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` X ) = ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` (/) ) ` X ) )
30 simpl
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> M e. V )
31 6 adantr
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( _E i^i ( M X. M ) ) e. _V )
32 simpr
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> X e. ( Fmla ` (/) ) )
33 eqid
 |-  ( M Sat ( _E i^i ( M X. M ) ) ) = ( M Sat ( _E i^i ( M X. M ) ) )
34 33 satfv0fvfmla0
 |-  ( ( M e. V /\ ( _E i^i ( M X. M ) ) e. _V /\ X e. ( Fmla ` (/) ) ) -> ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` (/) ) ` X ) = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) ( _E i^i ( M X. M ) ) ( a ` ( 2nd ` ( 2nd ` X ) ) ) } )
35 30 31 32 34 syl3anc
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` (/) ) ` X ) = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) ( _E i^i ( M X. M ) ) ( a ` ( 2nd ` ( 2nd ` X ) ) ) } )
36 elmapi
 |-  ( a e. ( M ^m _om ) -> a : _om --> M )
37 simpl
 |-  ( ( a : _om --> M /\ ( M e. V /\ X e. ( Fmla ` (/) ) ) ) -> a : _om --> M )
38 fmla0xp
 |-  ( Fmla ` (/) ) = ( { (/) } X. ( _om X. _om ) )
39 38 eleq2i
 |-  ( X e. ( Fmla ` (/) ) <-> X e. ( { (/) } X. ( _om X. _om ) ) )
40 elxp
 |-  ( X e. ( { (/) } X. ( _om X. _om ) ) <-> E. x E. y ( X = <. x , y >. /\ ( x e. { (/) } /\ y e. ( _om X. _om ) ) ) )
41 39 40 bitri
 |-  ( X e. ( Fmla ` (/) ) <-> E. x E. y ( X = <. x , y >. /\ ( x e. { (/) } /\ y e. ( _om X. _om ) ) ) )
42 xp1st
 |-  ( y e. ( _om X. _om ) -> ( 1st ` y ) e. _om )
43 42 ad2antll
 |-  ( ( X = <. x , y >. /\ ( x e. { (/) } /\ y e. ( _om X. _om ) ) ) -> ( 1st ` y ) e. _om )
44 vex
 |-  x e. _V
45 vex
 |-  y e. _V
46 44 45 op2ndd
 |-  ( X = <. x , y >. -> ( 2nd ` X ) = y )
47 46 fveq2d
 |-  ( X = <. x , y >. -> ( 1st ` ( 2nd ` X ) ) = ( 1st ` y ) )
48 47 eleq1d
 |-  ( X = <. x , y >. -> ( ( 1st ` ( 2nd ` X ) ) e. _om <-> ( 1st ` y ) e. _om ) )
49 48 adantr
 |-  ( ( X = <. x , y >. /\ ( x e. { (/) } /\ y e. ( _om X. _om ) ) ) -> ( ( 1st ` ( 2nd ` X ) ) e. _om <-> ( 1st ` y ) e. _om ) )
50 43 49 mpbird
 |-  ( ( X = <. x , y >. /\ ( x e. { (/) } /\ y e. ( _om X. _om ) ) ) -> ( 1st ` ( 2nd ` X ) ) e. _om )
51 50 exlimivv
 |-  ( E. x E. y ( X = <. x , y >. /\ ( x e. { (/) } /\ y e. ( _om X. _om ) ) ) -> ( 1st ` ( 2nd ` X ) ) e. _om )
52 41 51 sylbi
 |-  ( X e. ( Fmla ` (/) ) -> ( 1st ` ( 2nd ` X ) ) e. _om )
53 52 ad2antll
 |-  ( ( a : _om --> M /\ ( M e. V /\ X e. ( Fmla ` (/) ) ) ) -> ( 1st ` ( 2nd ` X ) ) e. _om )
54 37 53 ffvelrnd
 |-  ( ( a : _om --> M /\ ( M e. V /\ X e. ( Fmla ` (/) ) ) ) -> ( a ` ( 1st ` ( 2nd ` X ) ) ) e. M )
55 xp2nd
 |-  ( y e. ( _om X. _om ) -> ( 2nd ` y ) e. _om )
56 55 ad2antll
 |-  ( ( X = <. x , y >. /\ ( x e. { (/) } /\ y e. ( _om X. _om ) ) ) -> ( 2nd ` y ) e. _om )
57 46 fveq2d
 |-  ( X = <. x , y >. -> ( 2nd ` ( 2nd ` X ) ) = ( 2nd ` y ) )
58 57 eleq1d
 |-  ( X = <. x , y >. -> ( ( 2nd ` ( 2nd ` X ) ) e. _om <-> ( 2nd ` y ) e. _om ) )
59 58 adantr
 |-  ( ( X = <. x , y >. /\ ( x e. { (/) } /\ y e. ( _om X. _om ) ) ) -> ( ( 2nd ` ( 2nd ` X ) ) e. _om <-> ( 2nd ` y ) e. _om ) )
60 56 59 mpbird
 |-  ( ( X = <. x , y >. /\ ( x e. { (/) } /\ y e. ( _om X. _om ) ) ) -> ( 2nd ` ( 2nd ` X ) ) e. _om )
61 60 exlimivv
 |-  ( E. x E. y ( X = <. x , y >. /\ ( x e. { (/) } /\ y e. ( _om X. _om ) ) ) -> ( 2nd ` ( 2nd ` X ) ) e. _om )
62 41 61 sylbi
 |-  ( X e. ( Fmla ` (/) ) -> ( 2nd ` ( 2nd ` X ) ) e. _om )
63 62 ad2antll
 |-  ( ( a : _om --> M /\ ( M e. V /\ X e. ( Fmla ` (/) ) ) ) -> ( 2nd ` ( 2nd ` X ) ) e. _om )
64 37 63 ffvelrnd
 |-  ( ( a : _om --> M /\ ( M e. V /\ X e. ( Fmla ` (/) ) ) ) -> ( a ` ( 2nd ` ( 2nd ` X ) ) ) e. M )
65 54 64 jca
 |-  ( ( a : _om --> M /\ ( M e. V /\ X e. ( Fmla ` (/) ) ) ) -> ( ( a ` ( 1st ` ( 2nd ` X ) ) ) e. M /\ ( a ` ( 2nd ` ( 2nd ` X ) ) ) e. M ) )
66 65 ex
 |-  ( a : _om --> M -> ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( ( a ` ( 1st ` ( 2nd ` X ) ) ) e. M /\ ( a ` ( 2nd ` ( 2nd ` X ) ) ) e. M ) ) )
67 36 66 syl
 |-  ( a e. ( M ^m _om ) -> ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( ( a ` ( 1st ` ( 2nd ` X ) ) ) e. M /\ ( a ` ( 2nd ` ( 2nd ` X ) ) ) e. M ) ) )
68 67 impcom
 |-  ( ( ( M e. V /\ X e. ( Fmla ` (/) ) ) /\ a e. ( M ^m _om ) ) -> ( ( a ` ( 1st ` ( 2nd ` X ) ) ) e. M /\ ( a ` ( 2nd ` ( 2nd ` X ) ) ) e. M ) )
69 brinxp
 |-  ( ( ( a ` ( 1st ` ( 2nd ` X ) ) ) e. M /\ ( a ` ( 2nd ` ( 2nd ` X ) ) ) e. M ) -> ( ( a ` ( 1st ` ( 2nd ` X ) ) ) _E ( a ` ( 2nd ` ( 2nd ` X ) ) ) <-> ( a ` ( 1st ` ( 2nd ` X ) ) ) ( _E i^i ( M X. M ) ) ( a ` ( 2nd ` ( 2nd ` X ) ) ) ) )
70 69 bicomd
 |-  ( ( ( a ` ( 1st ` ( 2nd ` X ) ) ) e. M /\ ( a ` ( 2nd ` ( 2nd ` X ) ) ) e. M ) -> ( ( a ` ( 1st ` ( 2nd ` X ) ) ) ( _E i^i ( M X. M ) ) ( a ` ( 2nd ` ( 2nd ` X ) ) ) <-> ( a ` ( 1st ` ( 2nd ` X ) ) ) _E ( a ` ( 2nd ` ( 2nd ` X ) ) ) ) )
71 68 70 syl
 |-  ( ( ( M e. V /\ X e. ( Fmla ` (/) ) ) /\ a e. ( M ^m _om ) ) -> ( ( a ` ( 1st ` ( 2nd ` X ) ) ) ( _E i^i ( M X. M ) ) ( a ` ( 2nd ` ( 2nd ` X ) ) ) <-> ( a ` ( 1st ` ( 2nd ` X ) ) ) _E ( a ` ( 2nd ` ( 2nd ` X ) ) ) ) )
72 fvex
 |-  ( a ` ( 2nd ` ( 2nd ` X ) ) ) e. _V
73 72 epeli
 |-  ( ( a ` ( 1st ` ( 2nd ` X ) ) ) _E ( a ` ( 2nd ` ( 2nd ` X ) ) ) <-> ( a ` ( 1st ` ( 2nd ` X ) ) ) e. ( a ` ( 2nd ` ( 2nd ` X ) ) ) )
74 71 73 bitrdi
 |-  ( ( ( M e. V /\ X e. ( Fmla ` (/) ) ) /\ a e. ( M ^m _om ) ) -> ( ( a ` ( 1st ` ( 2nd ` X ) ) ) ( _E i^i ( M X. M ) ) ( a ` ( 2nd ` ( 2nd ` X ) ) ) <-> ( a ` ( 1st ` ( 2nd ` X ) ) ) e. ( a ` ( 2nd ` ( 2nd ` X ) ) ) ) )
75 74 rabbidva
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) ( _E i^i ( M X. M ) ) ( a ` ( 2nd ` ( 2nd ` X ) ) ) } = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) e. ( a ` ( 2nd ` ( 2nd ` X ) ) ) } )
76 35 75 eqtrd
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` (/) ) ` X ) = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) e. ( a ` ( 2nd ` ( 2nd ` X ) ) ) } )
77 29 76 eqtrd
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( ( ( M Sat ( _E i^i ( M X. M ) ) ) ` _om ) ` X ) = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) e. ( a ` ( 2nd ` ( 2nd ` X ) ) ) } )
78 1 77 eqtrd
 |-  ( ( M e. V /\ X e. ( Fmla ` (/) ) ) -> ( M SatE X ) = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` X ) ) ) e. ( a ` ( 2nd ` ( 2nd ` X ) ) ) } )