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 ffvelcdmd ⊢ 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 ffvelcdmd ⊢ 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