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 ) ) ) } )