Metamath Proof Explorer

Theorem sategoelfvb

Description: Characterization of a valuation S of a simplified satisfaction predicate for a Godel-set of membership. (Contributed by AV, 5-Nov-2023)

Ref Expression
Hypothesis sategoelfvb.s 
|- E = ( M SatE ( A e.g B ) )
Assertion sategoelfvb 
|- ( ( M e. V /\ ( A e. _om /\ B e. _om ) ) -> ( S e. E <-> ( S e. ( M ^m _om ) /\ ( S ` A ) e. ( S ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 sategoelfvb.s 
 |-  E = ( M SatE ( A e.g B ) )
2 ovexd 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A e.g B ) e. _V )
3 simpl 
 |-  ( ( A e. _om /\ B e. _om ) -> A e. _om )
4 opeq1 
 |-  ( a = A -> <. a , b >. = <. A , b >. )
5 4 opeq2d 
 |-  ( a = A -> <. (/) , <. a , b >. >. = <. (/) , <. A , b >. >. )
6 5 eqeq2d 
 |-  ( a = A -> ( <. (/) , <. A , B >. >. = <. (/) , <. a , b >. >. <-> <. (/) , <. A , B >. >. = <. (/) , <. A , b >. >. ) )
7 6 rexbidv 
 |-  ( a = A -> ( E. b e. _om <. (/) , <. A , B >. >. = <. (/) , <. a , b >. >. <-> E. b e. _om <. (/) , <. A , B >. >. = <. (/) , <. A , b >. >. ) )
8 7 adantl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ a = A ) -> ( E. b e. _om <. (/) , <. A , B >. >. = <. (/) , <. a , b >. >. <-> E. b e. _om <. (/) , <. A , B >. >. = <. (/) , <. A , b >. >. ) )
9 simpr 
 |-  ( ( A e. _om /\ B e. _om ) -> B e. _om )
10 opeq2 
 |-  ( b = B -> <. A , b >. = <. A , B >. )
11 10 opeq2d 
 |-  ( b = B -> <. (/) , <. A , b >. >. = <. (/) , <. A , B >. >. )
12 11 eqeq2d 
 |-  ( b = B -> ( <. (/) , <. A , B >. >. = <. (/) , <. A , b >. >. <-> <. (/) , <. A , B >. >. = <. (/) , <. A , B >. >. ) )
13 12 adantl 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ b = B ) -> ( <. (/) , <. A , B >. >. = <. (/) , <. A , b >. >. <-> <. (/) , <. A , B >. >. = <. (/) , <. A , B >. >. ) )
14 eqidd 
 |-  ( ( A e. _om /\ B e. _om ) -> <. (/) , <. A , B >. >. = <. (/) , <. A , B >. >. )
15 9 13 14 rspcedvd 
 |-  ( ( A e. _om /\ B e. _om ) -> E. b e. _om <. (/) , <. A , B >. >. = <. (/) , <. A , b >. >. )
16 3 8 15 rspcedvd 
 |-  ( ( A e. _om /\ B e. _om ) -> E. a e. _om E. b e. _om <. (/) , <. A , B >. >. = <. (/) , <. a , b >. >. )
17 goel 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A e.g B ) = <. (/) , <. A , B >. >. )
18 goel 
 |-  ( ( a e. _om /\ b e. _om ) -> ( a e.g b ) = <. (/) , <. a , b >. >. )
19 17 18 eqeqan12d 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ ( a e. _om /\ b e. _om ) ) -> ( ( A e.g B ) = ( a e.g b ) <-> <. (/) , <. A , B >. >. = <. (/) , <. a , b >. >. ) )
20 19 2rexbidva 
 |-  ( ( A e. _om /\ B e. _om ) -> ( E. a e. _om E. b e. _om ( A e.g B ) = ( a e.g b ) <-> E. a e. _om E. b e. _om <. (/) , <. A , B >. >. = <. (/) , <. a , b >. >. ) )
21 16 20 mpbird 
 |-  ( ( A e. _om /\ B e. _om ) -> E. a e. _om E. b e. _om ( A e.g B ) = ( a e.g b ) )
22 eqeq1 
 |-  ( x = ( A e.g B ) -> ( x = ( a e.g b ) <-> ( A e.g B ) = ( a e.g b ) ) )
23 22 2rexbidv 
 |-  ( x = ( A e.g B ) -> ( E. a e. _om E. b e. _om x = ( a e.g b ) <-> E. a e. _om E. b e. _om ( A e.g B ) = ( a e.g b ) ) )
24 fmla0 
 |-  ( Fmla ` (/) ) = { x e. _V | E. a e. _om E. b e. _om x = ( a e.g b ) }
25 23 24 elrab2 
 |-  ( ( A e.g B ) e. ( Fmla ` (/) ) <-> ( ( A e.g B ) e. _V /\ E. a e. _om E. b e. _om ( A e.g B ) = ( a e.g b ) ) )
26 2 21 25 sylanbrc 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A e.g B ) e. ( Fmla ` (/) ) )
27 satefvfmla0 
 |-  ( ( M e. V /\ ( A e.g B ) e. ( Fmla ` (/) ) ) -> ( M SatE ( A e.g B ) ) = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) e. ( a ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) } )
28 26 27 sylan2 
 |-  ( ( M e. V /\ ( A e. _om /\ B e. _om ) ) -> ( M SatE ( A e.g B ) ) = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) e. ( a ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) } )
29 1 28 syl5eq 
 |-  ( ( M e. V /\ ( A e. _om /\ B e. _om ) ) -> E = { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) e. ( a ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) } )
30 29 eleq2d 
 |-  ( ( M e. V /\ ( A e. _om /\ B e. _om ) ) -> ( S e. E <-> S e. { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) e. ( a ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) } ) )
31 fveq1 
 |-  ( a = S -> ( a ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) = ( S ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) )
32 fveq1 
 |-  ( a = S -> ( a ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) = ( S ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) )
33 31 32 eleq12d 
 |-  ( a = S -> ( ( a ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) e. ( a ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) <-> ( S ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) e. ( S ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) ) )
34 33 elrab 
 |-  ( S e. { a e. ( M ^m _om ) | ( a ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) e. ( a ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) } <-> ( S e. ( M ^m _om ) /\ ( S ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) e. ( S ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) ) )
35 30 34 bitrdi 
 |-  ( ( M e. V /\ ( A e. _om /\ B e. _om ) ) -> ( S e. E <-> ( S e. ( M ^m _om ) /\ ( S ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) e. ( S ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) ) ) )
36 17 fveq2d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( 2nd ` ( A e.g B ) ) = ( 2nd ` <. (/) , <. A , B >. >. ) )
37 36 fveq2d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( 1st ` ( 2nd ` ( A e.g B ) ) ) = ( 1st ` ( 2nd ` <. (/) , <. A , B >. >. ) ) )
38 0ex 
 |-  (/) e. _V
39 opex 
 |-  <. A , B >. e. _V
40 38 39 op2nd 
 |-  ( 2nd ` <. (/) , <. A , B >. >. ) = <. A , B >.
41 40 fveq2i 
 |-  ( 1st ` ( 2nd ` <. (/) , <. A , B >. >. ) ) = ( 1st ` <. A , B >. )
42 op1stg 
 |-  ( ( A e. _om /\ B e. _om ) -> ( 1st ` <. A , B >. ) = A )
43 41 42 syl5eq 
 |-  ( ( A e. _om /\ B e. _om ) -> ( 1st ` ( 2nd ` <. (/) , <. A , B >. >. ) ) = A )
44 37 43 eqtrd 
 |-  ( ( A e. _om /\ B e. _om ) -> ( 1st ` ( 2nd ` ( A e.g B ) ) ) = A )
45 44 fveq2d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( S ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) = ( S ` A ) )
46 36 fveq2d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( 2nd ` ( 2nd ` ( A e.g B ) ) ) = ( 2nd ` ( 2nd ` <. (/) , <. A , B >. >. ) ) )
47 40 fveq2i 
 |-  ( 2nd ` ( 2nd ` <. (/) , <. A , B >. >. ) ) = ( 2nd ` <. A , B >. )
48 op2ndg 
 |-  ( ( A e. _om /\ B e. _om ) -> ( 2nd ` <. A , B >. ) = B )
49 47 48 syl5eq 
 |-  ( ( A e. _om /\ B e. _om ) -> ( 2nd ` ( 2nd ` <. (/) , <. A , B >. >. ) ) = B )
50 46 49 eqtrd 
 |-  ( ( A e. _om /\ B e. _om ) -> ( 2nd ` ( 2nd ` ( A e.g B ) ) ) = B )
51 50 fveq2d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( S ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) = ( S ` B ) )
52 45 51 eleq12d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( S ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) e. ( S ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) <-> ( S ` A ) e. ( S ` B ) ) )
53 52 adantl 
 |-  ( ( M e. V /\ ( A e. _om /\ B e. _om ) ) -> ( ( S ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) e. ( S ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) <-> ( S ` A ) e. ( S ` B ) ) )
54 53 anbi2d 
 |-  ( ( M e. V /\ ( A e. _om /\ B e. _om ) ) -> ( ( S e. ( M ^m _om ) /\ ( S ` ( 1st ` ( 2nd ` ( A e.g B ) ) ) ) e. ( S ` ( 2nd ` ( 2nd ` ( A e.g B ) ) ) ) ) <-> ( S e. ( M ^m _om ) /\ ( S ` A ) e. ( S ` B ) ) ) )
55 35 54 bitrd 
 |-  ( ( M e. V /\ ( A e. _om /\ B e. _om ) ) -> ( S e. E <-> ( S e. ( M ^m _om ) /\ ( S ` A ) e. ( S ` B ) ) ) )