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 V X Fmla M Sat X = a M ω | a 1 st 2 nd X a 2 nd 2 nd X

Proof

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