Metamath Proof Explorer


Theorem satfrnmapom

Description: The range of the satisfaction predicate as function over wff codes in any model M and any binary relation E on M for a natural number N is a subset of the power set of all mappings from the natural numbers into the model M . (Contributed by AV, 13-Oct-2023)

Ref Expression
Assertion satfrnmapom M V E W N ω ran M Sat E N 𝒫 M ω

Proof

Step Hyp Ref Expression
1 fveq2 a = M Sat E a = M Sat E
2 1 rneqd a = ran M Sat E a = ran M Sat E
3 2 eleq2d a = n ran M Sat E a n ran M Sat E
4 3 imbi1d a = n ran M Sat E a n 𝒫 M ω n ran M Sat E n 𝒫 M ω
5 4 imbi2d a = M V E W n ran M Sat E a n 𝒫 M ω M V E W n ran M Sat E n 𝒫 M ω
6 fveq2 a = b M Sat E a = M Sat E b
7 6 rneqd a = b ran M Sat E a = ran M Sat E b
8 7 eleq2d a = b n ran M Sat E a n ran M Sat E b
9 8 imbi1d a = b n ran M Sat E a n 𝒫 M ω n ran M Sat E b n 𝒫 M ω
10 9 imbi2d a = b M V E W n ran M Sat E a n 𝒫 M ω M V E W n ran M Sat E b n 𝒫 M ω
11 fveq2 a = suc b M Sat E a = M Sat E suc b
12 11 rneqd a = suc b ran M Sat E a = ran M Sat E suc b
13 12 eleq2d a = suc b n ran M Sat E a n ran M Sat E suc b
14 13 imbi1d a = suc b n ran M Sat E a n 𝒫 M ω n ran M Sat E suc b n 𝒫 M ω
15 14 imbi2d a = suc b M V E W n ran M Sat E a n 𝒫 M ω M V E W n ran M Sat E suc b n 𝒫 M ω
16 fveq2 a = N M Sat E a = M Sat E N
17 16 rneqd a = N ran M Sat E a = ran M Sat E N
18 17 eleq2d a = N n ran M Sat E a n ran M Sat E N
19 18 imbi1d a = N n ran M Sat E a n 𝒫 M ω n ran M Sat E N n 𝒫 M ω
20 19 imbi2d a = N M V E W n ran M Sat E a n 𝒫 M ω M V E W n ran M Sat E N n 𝒫 M ω
21 eqid M Sat E = M Sat E
22 21 satfv0 M V E W M Sat E = x y | i ω j ω x = i 𝑔 j y = f M ω | f i E f j
23 22 rneqd M V E W ran M Sat E = ran x y | i ω j ω x = i 𝑔 j y = f M ω | f i E f j
24 23 eleq2d M V E W n ran M Sat E n ran x y | i ω j ω x = i 𝑔 j y = f M ω | f i E f j
25 rnopab ran x y | i ω j ω x = i 𝑔 j y = f M ω | f i E f j = y | x i ω j ω x = i 𝑔 j y = f M ω | f i E f j
26 25 eleq2i n ran x y | i ω j ω x = i 𝑔 j y = f M ω | f i E f j n y | x i ω j ω x = i 𝑔 j y = f M ω | f i E f j
27 vex n V
28 eqeq1 y = n y = f M ω | f i E f j n = f M ω | f i E f j
29 28 anbi2d y = n x = i 𝑔 j y = f M ω | f i E f j x = i 𝑔 j n = f M ω | f i E f j
30 29 2rexbidv y = n i ω j ω x = i 𝑔 j y = f M ω | f i E f j i ω j ω x = i 𝑔 j n = f M ω | f i E f j
31 30 exbidv y = n x i ω j ω x = i 𝑔 j y = f M ω | f i E f j x i ω j ω x = i 𝑔 j n = f M ω | f i E f j
32 27 31 elab n y | x i ω j ω x = i 𝑔 j y = f M ω | f i E f j x i ω j ω x = i 𝑔 j n = f M ω | f i E f j
33 ovex M ω V
34 ssrab2 f M ω | f i E f j M ω
35 33 34 elpwi2 f M ω | f i E f j 𝒫 M ω
36 eleq1 n = f M ω | f i E f j n 𝒫 M ω f M ω | f i E f j 𝒫 M ω
37 35 36 mpbiri n = f M ω | f i E f j n 𝒫 M ω
38 37 adantl x = i 𝑔 j n = f M ω | f i E f j n 𝒫 M ω
39 38 a1i i ω j ω x = i 𝑔 j n = f M ω | f i E f j n 𝒫 M ω
40 39 rexlimivv i ω j ω x = i 𝑔 j n = f M ω | f i E f j n 𝒫 M ω
41 40 exlimiv x i ω j ω x = i 𝑔 j n = f M ω | f i E f j n 𝒫 M ω
42 32 41 sylbi n y | x i ω j ω x = i 𝑔 j y = f M ω | f i E f j n 𝒫 M ω
43 42 a1i M V E W n y | x i ω j ω x = i 𝑔 j y = f M ω | f i E f j n 𝒫 M ω
44 26 43 syl5bi M V E W n ran x y | i ω j ω x = i 𝑔 j y = f M ω | f i E f j n 𝒫 M ω
45 24 44 sylbid M V E W n ran M Sat E n 𝒫 M ω
46 21 satfvsuc M V E W b ω M Sat E suc b = M Sat E b x y | u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u
47 46 3expa M V E W b ω M Sat E suc b = M Sat E b x y | u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u
48 47 rneqd M V E W b ω ran M Sat E suc b = ran M Sat E b x y | u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u
49 rnun ran M Sat E b x y | u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u = ran M Sat E b ran x y | u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u
50 48 49 eqtrdi M V E W b ω ran M Sat E suc b = ran M Sat E b ran x y | u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u
51 50 eleq2d M V E W b ω n ran M Sat E suc b n ran M Sat E b ran x y | u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u
52 elun n ran M Sat E b ran x y | u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u n ran M Sat E b n ran x y | u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u
53 rnopab ran x y | u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u = y | x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u
54 53 eleq2i n ran x y | u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u n y | x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u
55 eqeq1 y = n y = M ω 2 nd u 2 nd v n = M ω 2 nd u 2 nd v
56 55 anbi2d y = n x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v
57 56 rexbidv y = n v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v
58 eqeq1 y = n y = a M ω | z M i z a ω i 2 nd u n = a M ω | z M i z a ω i 2 nd u
59 58 anbi2d y = n x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u
60 59 rexbidv y = n i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u
61 57 60 orbi12d y = n v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u
62 61 rexbidv y = n u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u
63 62 exbidv y = n x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u
64 27 63 elab n y | x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u
65 54 64 bitri n ran x y | u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u
66 65 orbi2i n ran M Sat E b n ran x y | u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u n ran M Sat E b x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u
67 52 66 bitri n ran M Sat E b ran x y | u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = a M ω | z M i z a ω i 2 nd u n ran M Sat E b x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u
68 51 67 bitrdi M V E W b ω n ran M Sat E suc b n ran M Sat E b x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u
69 68 expcom b ω M V E W n ran M Sat E suc b n ran M Sat E b x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u
70 69 adantr b ω M V E W n ran M Sat E b n 𝒫 M ω M V E W n ran M Sat E suc b n ran M Sat E b x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u
71 70 imp b ω M V E W n ran M Sat E b n 𝒫 M ω M V E W n ran M Sat E suc b n ran M Sat E b x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u
72 simpr b ω M V E W n ran M Sat E b n 𝒫 M ω M V E W n ran M Sat E b n 𝒫 M ω
73 72 imp b ω M V E W n ran M Sat E b n 𝒫 M ω M V E W n ran M Sat E b n 𝒫 M ω
74 difss M ω 2 nd u 2 nd v M ω
75 33 74 elpwi2 M ω 2 nd u 2 nd v 𝒫 M ω
76 eleq1 n = M ω 2 nd u 2 nd v n 𝒫 M ω M ω 2 nd u 2 nd v 𝒫 M ω
77 75 76 mpbiri n = M ω 2 nd u 2 nd v n 𝒫 M ω
78 77 adantl x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v n 𝒫 M ω
79 78 adantl v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v n 𝒫 M ω
80 79 rexlimiva v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v n 𝒫 M ω
81 ssrab2 a M ω | z M i z a ω i 2 nd u M ω
82 33 81 elpwi2 a M ω | z M i z a ω i 2 nd u 𝒫 M ω
83 eleq1 n = a M ω | z M i z a ω i 2 nd u n 𝒫 M ω a M ω | z M i z a ω i 2 nd u 𝒫 M ω
84 82 83 mpbiri n = a M ω | z M i z a ω i 2 nd u n 𝒫 M ω
85 84 adantl x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u n 𝒫 M ω
86 85 a1i i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u n 𝒫 M ω
87 86 rexlimiv i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u n 𝒫 M ω
88 80 87 jaoi v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u n 𝒫 M ω
89 88 a1i u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u n 𝒫 M ω
90 89 rexlimiv u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u n 𝒫 M ω
91 90 exlimiv x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u n 𝒫 M ω
92 91 a1i b ω M V E W n ran M Sat E b n 𝒫 M ω M V E W x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u n 𝒫 M ω
93 73 92 jaod b ω M V E W n ran M Sat E b n 𝒫 M ω M V E W n ran M Sat E b x u M Sat E b v M Sat E b x = 1 st u 𝑔 1 st v n = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u n = a M ω | z M i z a ω i 2 nd u n 𝒫 M ω
94 71 93 sylbid b ω M V E W n ran M Sat E b n 𝒫 M ω M V E W n ran M Sat E suc b n 𝒫 M ω
95 94 exp31 b ω M V E W n ran M Sat E b n 𝒫 M ω M V E W n ran M Sat E suc b n 𝒫 M ω
96 5 10 15 20 45 95 finds N ω M V E W n ran M Sat E N n 𝒫 M ω
97 96 com12 M V E W N ω n ran M Sat E N n 𝒫 M ω
98 97 3impia M V E W N ω n ran M Sat E N n 𝒫 M ω
99 98 ssrdv M V E W N ω ran M Sat E N 𝒫 M ω