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⁡∅→MSat∈X=a∈Mω|a⁡1st⁡2nd⁡X∈a⁡2nd⁡2nd⁡X

Proof

Step Hyp Ref Expression
1 satefv ⊢M∈V∧X∈Fmla⁡∅→MSat∈X=MSatE∩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→MSatE∩M×M⁡ω=⋃i∈ωMSatE∩M×M⁡i
10 8 9 syl ⊢M∈V∧X∈Fmla⁡∅→MSatE∩M×M⁡ω=⋃i∈ωMSatE∩M×M⁡i
11 10 fveq1d ⊢M∈V∧X∈Fmla⁡∅→MSatE∩M×M⁡ω⁡X=⋃i∈ωMSatE∩M×M⁡i⁡X
12 satfun ⊢M∈V∧E∩M×M∈V→MSatE∩M×M⁡ω:Fmla⁡ω⟶𝒫Mω
13 8 12 syl ⊢M∈V∧X∈Fmla⁡∅→MSatE∩M×M⁡ω:Fmla⁡ω⟶𝒫Mω
14 13 ffund ⊢M∈V∧X∈Fmla⁡∅→Fun⁡MSatE∩M×M⁡ω
15 10 eqcomd ⊢M∈V∧X∈Fmla⁡∅→⋃i∈ωMSatE∩M×M⁡i=MSatE∩M×M⁡ω
16 15 funeqd ⊢M∈V∧X∈Fmla⁡∅→Fun⁡⋃i∈ωMSatE∩M×M⁡i↔Fun⁡MSatE∩M×M⁡ω
17 14 16 mpbird ⊢M∈V∧X∈Fmla⁡∅→Fun⁡⋃i∈ωMSatE∩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⁡MSatE∩M×M⁡∅=Fmla⁡∅
22 6 20 21 mpd3an23 ⊢M∈V→dom⁡MSatE∩M×M⁡∅=Fmla⁡∅
23 22 eqcomd ⊢M∈V→Fmla⁡∅=dom⁡MSatE∩M×M⁡∅
24 23 eleq2d ⊢M∈V→X∈Fmla⁡∅↔X∈dom⁡MSatE∩M×M⁡∅
25 24 biimpa ⊢M∈V∧X∈Fmla⁡∅→X∈dom⁡MSatE∩M×M⁡∅
26 eqid ⊢⋃i∈ωMSatE∩M×M⁡i=⋃i∈ωMSatE∩M×M⁡i
27 26 fviunfun ⊢Fun⁡⋃i∈ωMSatE∩M×M⁡i∧∅∈ω∧X∈dom⁡MSatE∩M×M⁡∅→⋃i∈ωMSatE∩M×M⁡i⁡X=MSatE∩M×M⁡∅⁡X
28 17 19 25 27 syl3anc ⊢M∈V∧X∈Fmla⁡∅→⋃i∈ωMSatE∩M×M⁡i⁡X=MSatE∩M×M⁡∅⁡X
29 11 28 eqtrd ⊢M∈V∧X∈Fmla⁡∅→MSatE∩M×M⁡ω⁡X=MSatE∩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 ⊢MSatE∩M×M=MSatE∩M×M
34 33 satfv0fvfmla0 ⊢M∈V∧E∩M×M∈V∧X∈Fmla⁡∅→MSatE∩M×M⁡∅⁡X=a∈Mω|a⁡1st⁡2nd⁡XE∩M×Ma⁡2nd⁡2nd⁡X
35 30 31 32 34 syl3anc ⊢M∈V∧X∈Fmla⁡∅→MSatE∩M×M⁡∅⁡X=a∈Mω|a⁡1st⁡2nd⁡XE∩M×Ma⁡2nd⁡2nd⁡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∃yX=xy∧x∈∅∧y∈ω×ω
41 39 40 bitri ⊢X∈Fmla⁡∅↔∃x∃yX=xy∧x∈∅∧y∈ω×ω
42 xp1st ⊢y∈ω×ω→1st⁡y∈ω
43 42 ad2antll ⊢X=xy∧x∈∅∧y∈ω×ω→1st⁡y∈ω
44 vex ⊢x∈V
45 vex ⊢y∈V
46 44 45 op2ndd ⊢X=xy→2nd⁡X=y
47 46 fveq2d ⊢X=xy→1st⁡2nd⁡X=1st⁡y
48 47 eleq1d ⊢X=xy→1st⁡2nd⁡X∈ω↔1st⁡y∈ω
49 48 adantr ⊢X=xy∧x∈∅∧y∈ω×ω→1st⁡2nd⁡X∈ω↔1st⁡y∈ω
50 43 49 mpbird ⊢X=xy∧x∈∅∧y∈ω×ω→1st⁡2nd⁡X∈ω
51 50 exlimivv ⊢∃x∃yX=xy∧x∈∅∧y∈ω×ω→1st⁡2nd⁡X∈ω
52 41 51 sylbi ⊢X∈Fmla⁡∅→1st⁡2nd⁡X∈ω
53 52 ad2antll ⊢a:ω⟶M∧M∈V∧X∈Fmla⁡∅→1st⁡2nd⁡X∈ω
54 37 53 ffvelcdmd ⊢a:ω⟶M∧M∈V∧X∈Fmla⁡∅→a⁡1st⁡2nd⁡X∈M
55 xp2nd ⊢y∈ω×ω→2nd⁡y∈ω
56 55 ad2antll ⊢X=xy∧x∈∅∧y∈ω×ω→2nd⁡y∈ω
57 46 fveq2d ⊢X=xy→2nd⁡2nd⁡X=2nd⁡y
58 57 eleq1d ⊢X=xy→2nd⁡2nd⁡X∈ω↔2nd⁡y∈ω
59 58 adantr ⊢X=xy∧x∈∅∧y∈ω×ω→2nd⁡2nd⁡X∈ω↔2nd⁡y∈ω
60 56 59 mpbird ⊢X=xy∧x∈∅∧y∈ω×ω→2nd⁡2nd⁡X∈ω
61 60 exlimivv ⊢∃x∃yX=xy∧x∈∅∧y∈ω×ω→2nd⁡2nd⁡X∈ω
62 41 61 sylbi ⊢X∈Fmla⁡∅→2nd⁡2nd⁡X∈ω
63 62 ad2antll ⊢a:ω⟶M∧M∈V∧X∈Fmla⁡∅→2nd⁡2nd⁡X∈ω
64 37 63 ffvelcdmd ⊢a:ω⟶M∧M∈V∧X∈Fmla⁡∅→a⁡2nd⁡2nd⁡X∈M
65 54 64 jca ⊢a:ω⟶M∧M∈V∧X∈Fmla⁡∅→a⁡1st⁡2nd⁡X∈M∧a⁡2nd⁡2nd⁡X∈M
66 65 ex ⊢a:ω⟶M→M∈V∧X∈Fmla⁡∅→a⁡1st⁡2nd⁡X∈M∧a⁡2nd⁡2nd⁡X∈M
67 36 66 syl ⊢a∈Mω→M∈V∧X∈Fmla⁡∅→a⁡1st⁡2nd⁡X∈M∧a⁡2nd⁡2nd⁡X∈M
68 67 impcom ⊢M∈V∧X∈Fmla⁡∅∧a∈Mω→a⁡1st⁡2nd⁡X∈M∧a⁡2nd⁡2nd⁡X∈M
69 brinxp ⊢a⁡1st⁡2nd⁡X∈M∧a⁡2nd⁡2nd⁡X∈M→a⁡1st⁡2nd⁡XEa⁡2nd⁡2nd⁡X↔a⁡1st⁡2nd⁡XE∩M×Ma⁡2nd⁡2nd⁡X
70 69 bicomd ⊢a⁡1st⁡2nd⁡X∈M∧a⁡2nd⁡2nd⁡X∈M→a⁡1st⁡2nd⁡XE∩M×Ma⁡2nd⁡2nd⁡X↔a⁡1st⁡2nd⁡XEa⁡2nd⁡2nd⁡X
71 68 70 syl ⊢M∈V∧X∈Fmla⁡∅∧a∈Mω→a⁡1st⁡2nd⁡XE∩M×Ma⁡2nd⁡2nd⁡X↔a⁡1st⁡2nd⁡XEa⁡2nd⁡2nd⁡X
72 fvex ⊢a⁡2nd⁡2nd⁡X∈V
73 72 epeli ⊢a⁡1st⁡2nd⁡XEa⁡2nd⁡2nd⁡X↔a⁡1st⁡2nd⁡X∈a⁡2nd⁡2nd⁡X
74 71 73 bitrdi ⊢M∈V∧X∈Fmla⁡∅∧a∈Mω→a⁡1st⁡2nd⁡XE∩M×Ma⁡2nd⁡2nd⁡X↔a⁡1st⁡2nd⁡X∈a⁡2nd⁡2nd⁡X
75 74 rabbidva ⊢M∈V∧X∈Fmla⁡∅→a∈Mω|a⁡1st⁡2nd⁡XE∩M×Ma⁡2nd⁡2nd⁡X=a∈Mω|a⁡1st⁡2nd⁡X∈a⁡2nd⁡2nd⁡X
76 35 75 eqtrd ⊢M∈V∧X∈Fmla⁡∅→MSatE∩M×M⁡∅⁡X=a∈Mω|a⁡1st⁡2nd⁡X∈a⁡2nd⁡2nd⁡X
77 29 76 eqtrd ⊢M∈V∧X∈Fmla⁡∅→MSatE∩M×M⁡ω⁡X=a∈Mω|a⁡1st⁡2nd⁡X∈a⁡2nd⁡2nd⁡X
78 1 77 eqtrd ⊢M∈V∧X∈Fmla⁡∅→MSat∈X=a∈Mω|a⁡1st⁡2nd⁡X∈a⁡2nd⁡2nd⁡X