Step | Hyp | Ref
| Expression |
1 | | satffunlem2lem2.s |
. . . . . 6
⊢ 𝑆 = (𝑀 Sat 𝐸) |
2 | 1 | fveq1i 6777 |
. . . . 5
⊢ (𝑆‘suc 𝑁) = ((𝑀 Sat 𝐸)‘suc 𝑁) |
3 | 2 | dmeqi 5815 |
. . . 4
⊢ dom
(𝑆‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁) |
4 | | simprl 768 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝑀 ∈ 𝑉) |
5 | | simprr 770 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝐸 ∈ 𝑊) |
6 | | peano2 7737 |
. . . . . . . 8
⊢ (𝑁 ∈ ω → suc 𝑁 ∈
ω) |
7 | 6 | adantr 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → suc 𝑁 ∈ ω) |
8 | 4, 5, 7 | 3jca 1127 |
. . . . . 6
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω)) |
9 | | satfdmfmla 33359 |
. . . . . 6
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁)) |
10 | 8, 9 | syl 17 |
. . . . 5
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁)) |
11 | 10 | adantr 481 |
. . . 4
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁)) |
12 | 3, 11 | eqtrid 2790 |
. . 3
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom (𝑆‘suc 𝑁) = (Fmla‘suc 𝑁)) |
13 | | satffunlem2lem2.a |
. . . . . . . . . 10
⊢ 𝐴 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) |
14 | | ovex 7310 |
. . . . . . . . . . 11
⊢ (𝑀 ↑m ω)
∈ V |
15 | 14 | difexi 5254 |
. . . . . . . . . 10
⊢ ((𝑀 ↑m ω)
∖ ((2nd ‘𝑢) ∩ (2nd ‘𝑣))) ∈ V |
16 | 13, 15 | eqeltri 2835 |
. . . . . . . . 9
⊢ 𝐴 ∈ V |
17 | 16 | a1i 11 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → 𝐴 ∈ V) |
18 | 17 | ralrimiva 3103 |
. . . . . . 7
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → ∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V) |
19 | | satffunlem2lem2.b |
. . . . . . . . . 10
⊢ 𝐵 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} |
20 | 19, 14 | rabex2 5260 |
. . . . . . . . 9
⊢ 𝐵 ∈ V |
21 | 20 | a1i 11 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) ∧ 𝑖 ∈ ω) → 𝐵 ∈ V) |
22 | 21 | ralrimiva 3103 |
. . . . . . 7
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → ∀𝑖 ∈ ω 𝐵 ∈ V) |
23 | 18, 22 | jca 512 |
. . . . . 6
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → (∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V ∧ ∀𝑖 ∈ ω 𝐵 ∈ V)) |
24 | 23 | ralrimiva 3103 |
. . . . 5
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ∀𝑢 ∈ (𝑆‘suc 𝑁)(∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V ∧ ∀𝑖 ∈ ω 𝐵 ∈ V)) |
25 | | simplr 766 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) |
26 | 6 | ancri 550 |
. . . . . . . 8
⊢ (𝑁 ∈ ω → (suc
𝑁 ∈ ω ∧
𝑁 ∈
ω)) |
27 | 26 | ad2antrr 723 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) |
28 | 25, 27 | jca 512 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω))) |
29 | | sssucid 6345 |
. . . . . 6
⊢ 𝑁 ⊆ suc 𝑁 |
30 | 1 | satfsschain 33323 |
. . . . . 6
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) → (𝑁 ⊆ suc 𝑁 → (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁))) |
31 | 28, 29, 30 | mpisyl 21 |
. . . . 5
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) |
32 | | dmopab3rexdif 33364 |
. . . . 5
⊢
((∀𝑢 ∈
(𝑆‘suc 𝑁)(∀𝑣 ∈ (𝑆‘suc 𝑁)𝐴 ∈ V ∧ ∀𝑖 ∈ ω 𝐵 ∈ V) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → dom {〈𝑥, 𝑦〉 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴))} = {𝑥 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))}) |
33 | 24, 31, 32 | syl2anc 584 |
. . . 4
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom {〈𝑥, 𝑦〉 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴))} = {𝑥 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))}) |
34 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) |
35 | | fveqeq2 6785 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑢 → ((1st ‘𝑤) = (1st ‘𝑢) ↔ (1st
‘𝑢) = (1st
‘𝑢))) |
36 | 35 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) ∧ 𝑤 = 𝑢) → ((1st ‘𝑤) = (1st ‘𝑢) ↔ (1st
‘𝑢) = (1st
‘𝑢))) |
37 | | eqidd 2739 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1st ‘𝑢) = (1st ‘𝑢)) |
38 | 34, 36, 37 | rspcedvd 3564 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ∃𝑤 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑤) = (1st ‘𝑢)) |
39 | 2 | funeqi 6457 |
. . . . . . . . . . . . . . . . . . 19
⊢ (Fun
(𝑆‘suc 𝑁) ↔ Fun ((𝑀 Sat 𝐸)‘suc 𝑁)) |
40 | 39 | biimpi 215 |
. . . . . . . . . . . . . . . . . 18
⊢ (Fun
(𝑆‘suc 𝑁) → Fun ((𝑀 Sat 𝐸)‘suc 𝑁)) |
41 | 40 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Fun ((𝑀 Sat 𝐸)‘suc 𝑁)) |
42 | 1 | fveq1i 6777 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑆‘𝑁) = ((𝑀 Sat 𝐸)‘𝑁) |
43 | 31, 42, 2 | 3sstr3g 3966 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) |
44 | 41, 43 | jca 512 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁))) |
45 | 44 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁))) |
46 | | funeldmdif 7889 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → ((1st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) ↔ ∃𝑤 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑤) = (1st ‘𝑢))) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ((1st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) ↔ ∃𝑤 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑤) = (1st ‘𝑢))) |
48 | 38, 47 | mpbird 256 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))) |
49 | 48 | ex 413 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) → (1st ‘𝑢) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))) |
50 | 2, 42 | difeq12i 4056 |
. . . . . . . . . . . . . 14
⊢ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) = (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) |
51 | 50 | eleq2i 2830 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) |
52 | 51 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))) |
53 | 11 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁)) |
54 | | simpl 483 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → 𝑁 ∈ ω) |
55 | 4, 5, 54 | 3jca 1127 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω)) |
56 | | satfdmfmla 33359 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁)) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁)) |
58 | 57 | eqcomd 2744 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fmla‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁)) |
59 | 58 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁)) |
60 | 53, 59 | difeq12d 4059 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))) |
61 | 60 | eleq2d 2824 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((1st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ (1st
‘𝑢) ∈ (dom
((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))) |
62 | 49, 52, 61 | 3imtr4d 294 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (1st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))) |
63 | 62 | imp 407 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (1st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) |
64 | 63 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) → (1st ‘𝑢) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) |
65 | | oveq1 7284 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (1st ‘𝑢) → (𝑓⊼𝑔𝑔) = ((1st ‘𝑢)⊼𝑔𝑔)) |
66 | 65 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ (𝑓 = (1st ‘𝑢) → (𝑥 = (𝑓⊼𝑔𝑔) ↔ 𝑥 = ((1st ‘𝑢)⊼𝑔𝑔))) |
67 | 66 | rexbidv 3225 |
. . . . . . . . . . 11
⊢ (𝑓 = (1st ‘𝑢) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ↔ ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔𝑔))) |
68 | | eqidd 2739 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (1st ‘𝑢) → 𝑖 = 𝑖) |
69 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (1st ‘𝑢) → 𝑓 = (1st ‘𝑢)) |
70 | 68, 69 | goaleq12d 33310 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (1st ‘𝑢) →
∀𝑔𝑖𝑓 = ∀𝑔𝑖(1st ‘𝑢)) |
71 | 70 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ (𝑓 = (1st ‘𝑢) → (𝑥 = ∀𝑔𝑖𝑓 ↔ 𝑥 = ∀𝑔𝑖(1st ‘𝑢))) |
72 | 71 | rexbidv 3225 |
. . . . . . . . . . 11
⊢ (𝑓 = (1st ‘𝑢) → (∃𝑖 ∈ ω 𝑥 =
∀𝑔𝑖𝑓 ↔ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))) |
73 | 67, 72 | orbi12d 916 |
. . . . . . . . . 10
⊢ (𝑓 = (1st ‘𝑢) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))) |
74 | 73 | adantl 482 |
. . . . . . . . 9
⊢
((((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) ∧ 𝑓 = (1st ‘𝑢)) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))) |
75 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → 𝑀 ∈ 𝑉) |
76 | 5 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → 𝐸 ∈ 𝑊) |
77 | 6 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → suc 𝑁 ∈ ω) |
78 | 75, 76, 77 | 3jca 1127 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω)) |
79 | | satfrel 33326 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω) → Rel ((𝑀 Sat 𝐸)‘suc 𝑁)) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘suc 𝑁)) |
81 | 2 | releqi 5690 |
. . . . . . . . . . . . . . . . 17
⊢ (Rel
(𝑆‘suc 𝑁) ↔ Rel ((𝑀 Sat 𝐸)‘suc 𝑁)) |
82 | 80, 81 | sylibr 233 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel (𝑆‘suc 𝑁)) |
83 | | 1stdm 7881 |
. . . . . . . . . . . . . . . 16
⊢ ((Rel
(𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (1st ‘𝑣) ∈ dom (𝑆‘suc 𝑁)) |
84 | 82, 83 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (1st ‘𝑣) ∈ dom (𝑆‘suc 𝑁)) |
85 | 12 | eqcomd 2744 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom (𝑆‘suc 𝑁)) |
86 | 85 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom (𝑆‘suc 𝑁)) |
87 | 84, 86 | eleqtrrd 2842 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (1st ‘𝑣) ∈ (Fmla‘suc 𝑁)) |
88 | 87 | ad4ant13 748 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) →
(1st ‘𝑣)
∈ (Fmla‘suc 𝑁)) |
89 | | oveq2 7285 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (1st ‘𝑣) → ((1st
‘𝑢)⊼𝑔𝑔) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣))) |
90 | 89 | eqeq2d 2749 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (1st ‘𝑣) → (𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ↔ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
91 | 90 | adantl 482 |
. . . . . . . . . . . . 13
⊢
(((((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) ∧ 𝑔 = (1st ‘𝑣)) → (𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ↔ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
92 | | simpr 485 |
. . . . . . . . . . . . 13
⊢
((((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) → 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) |
93 | 88, 91, 92 | rspcedvd 3564 |
. . . . . . . . . . . 12
⊢
((((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) →
∃𝑔 ∈
(Fmla‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔𝑔)) |
94 | 93 | rexlimdva2 3215 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) →
∃𝑔 ∈
(Fmla‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔𝑔))) |
95 | 94 | orim1d 963 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)))) |
96 | 95 | imp 407 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢))) |
97 | 64, 74, 96 | rspcedvd 3564 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))) → ∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓)) |
98 | 97 | rexlimdva2 3215 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) → ∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓))) |
99 | 55 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω)) |
100 | | satfrel 33326 |
. . . . . . . . . . . . . 14
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ 𝑁 ∈ ω) → Rel ((𝑀 Sat 𝐸)‘𝑁)) |
101 | 99, 100 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘𝑁)) |
102 | 42 | releqi 5690 |
. . . . . . . . . . . . 13
⊢ (Rel
(𝑆‘𝑁) ↔ Rel ((𝑀 Sat 𝐸)‘𝑁)) |
103 | 101, 102 | sylibr 233 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel (𝑆‘𝑁)) |
104 | | 1stdm 7881 |
. . . . . . . . . . . 12
⊢ ((Rel
(𝑆‘𝑁) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1st ‘𝑢) ∈ dom (𝑆‘𝑁)) |
105 | 103, 104 | sylan 580 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1st ‘𝑢) ∈ dom (𝑆‘𝑁)) |
106 | 42 | dmeqi 5815 |
. . . . . . . . . . . . . 14
⊢ dom
(𝑆‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁) |
107 | 99, 56 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom ((𝑀 Sat 𝐸)‘𝑁) = (Fmla‘𝑁)) |
108 | 106, 107 | eqtrid 2790 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom (𝑆‘𝑁) = (Fmla‘𝑁)) |
109 | 108 | eqcomd 2744 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘𝑁) = dom (𝑆‘𝑁)) |
110 | 109 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (Fmla‘𝑁) = dom (𝑆‘𝑁)) |
111 | 105, 110 | eleqtrrd 2842 |
. . . . . . . . . 10
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (1st ‘𝑢) ∈ (Fmla‘𝑁)) |
112 | 111 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) →
(1st ‘𝑢)
∈ (Fmla‘𝑁)) |
113 | 66 | rexbidv 3225 |
. . . . . . . . . 10
⊢ (𝑓 = (1st ‘𝑢) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔𝑔))) |
114 | 113 | adantl 482 |
. . . . . . . . 9
⊢
((((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) ∧ 𝑓 = (1st ‘𝑢)) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔𝑔))) |
115 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) |
116 | | fveqeq2 6785 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑣 → ((1st ‘𝑡) = (1st ‘𝑣) ↔ (1st
‘𝑣) = (1st
‘𝑣))) |
117 | 116 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) ∧ 𝑡 = 𝑣) → ((1st ‘𝑡) = (1st ‘𝑣) ↔ (1st
‘𝑣) = (1st
‘𝑣))) |
118 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1st ‘𝑣) = (1st ‘𝑣)) |
119 | 115, 117,
118 | rspcedvd 3564 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ∃𝑡 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑡) = (1st ‘𝑣)) |
120 | 44 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (Fun ((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁))) |
121 | | funeldmdif 7889 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Fun
((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → ((1st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) ↔ ∃𝑡 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑡) = (1st ‘𝑣))) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → ((1st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) ↔ ∃𝑡 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑡) = (1st ‘𝑣))) |
123 | 119, 122 | mpbird 256 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) → (1st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))) |
124 | 123 | ex 413 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) → (1st ‘𝑣) ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))) |
125 | 50 | eleq2i 2830 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))) |
126 | 125 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ↔ 𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)))) |
127 | 10 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁)) |
128 | 127, 58 | difeq12d 4059 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))) |
129 | 128 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → ((1st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ (1st
‘𝑣) ∈ (dom
((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))) |
130 | 129 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((1st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ (1st
‘𝑣) ∈ (dom
((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))) |
131 | 124, 126,
130 | 3imtr4d 294 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (1st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))) |
132 | 131 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (1st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)))) |
133 | 132 | imp 407 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (1st ‘𝑣) ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))) |
134 | 133 | adantr 481 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) →
(1st ‘𝑣)
∈ ((Fmla‘suc 𝑁)
∖ (Fmla‘𝑁))) |
135 | 90 | adantl 482 |
. . . . . . . . . . 11
⊢
(((((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) ∧ 𝑔 = (1st ‘𝑣)) → (𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ↔ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
136 | | simpr 485 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) → 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) |
137 | 134, 135,
136 | rspcedvd 3564 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) →
∃𝑔 ∈
((Fmla‘suc 𝑁) ∖
(Fmla‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔𝑔)) |
138 | 137 | r19.29an 3216 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) →
∃𝑔 ∈
((Fmla‘suc 𝑁) ∖
(Fmla‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔𝑔)) |
139 | 112, 114,
138 | rspcedvd 3564 |
. . . . . . . 8
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) →
∃𝑓 ∈
(Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔)) |
140 | 139 | rexlimdva2 3215 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) →
∃𝑓 ∈
(Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔))) |
141 | 98, 140 | orim12d 962 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) →
(∃𝑓 ∈
((Fmla‘suc 𝑁) ∖
(Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔)))) |
142 | 8 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω)) |
143 | 9 | eqcomd 2744 |
. . . . . . . . . . . . 13
⊢ ((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊 ∧ suc 𝑁 ∈ ω) → (Fmla‘suc
𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁)) |
144 | 142, 143 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁)) |
145 | 107 | eqcomd 2744 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘𝑁) = dom ((𝑀 Sat 𝐸)‘𝑁)) |
146 | 144, 145 | difeq12d 4059 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) = (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁))) |
147 | 146 | eleq2d 2824 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ 𝑓 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))) |
148 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢ (𝑀 Sat 𝐸) = (𝑀 Sat 𝐸) |
149 | 148 | satfsschain 33323 |
. . . . . . . . . . . 12
⊢ (((𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (suc 𝑁 ∈ ω ∧ 𝑁 ∈ ω)) → (𝑁 ⊆ suc 𝑁 → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁))) |
150 | 28, 29, 149 | mpisyl 21 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) |
151 | | releldmdifi 7886 |
. . . . . . . . . . 11
⊢ ((Rel
((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → (𝑓 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) → ∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑢) = 𝑓)) |
152 | 80, 150, 151 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) → ∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑢) = 𝑓)) |
153 | 147, 152 | sylbid 239 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑢) = 𝑓)) |
154 | 50 | eqcomi 2747 |
. . . . . . . . . . 11
⊢ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁)) = ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) |
155 | 154 | rexeqi 3346 |
. . . . . . . . . 10
⊢
(∃𝑢 ∈
(((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑢) = 𝑓 ↔ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1st ‘𝑢) = 𝑓) |
156 | | r19.41v 3275 |
. . . . . . . . . . . 12
⊢
(∃𝑢 ∈
((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))((1st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓)) ↔ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓))) |
157 | | oveq1 7284 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑢) = 𝑓 → ((1st ‘𝑢)⊼𝑔𝑔) = (𝑓⊼𝑔𝑔)) |
158 | 157 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . 18
⊢
((1st ‘𝑢) = 𝑓 → (𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ↔ 𝑥 = (𝑓⊼𝑔𝑔))) |
159 | 158 | rexbidv 3225 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑢) = 𝑓 → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ↔ ∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔))) |
160 | | eqidd 2739 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑢) = 𝑓 → 𝑖 = 𝑖) |
161 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑢) = 𝑓 → (1st ‘𝑢) = 𝑓) |
162 | 160, 161 | goaleq12d 33310 |
. . . . . . . . . . . . . . . . . . 19
⊢
((1st ‘𝑢) = 𝑓 → ∀𝑔𝑖(1st ‘𝑢) =
∀𝑔𝑖𝑓) |
163 | 162 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . 18
⊢
((1st ‘𝑢) = 𝑓 → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ 𝑥 = ∀𝑔𝑖𝑓)) |
164 | 163 | rexbidv 3225 |
. . . . . . . . . . . . . . . . 17
⊢
((1st ‘𝑢) = 𝑓 → (∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ ∃𝑖 ∈ ω 𝑥 =
∀𝑔𝑖𝑓)) |
165 | 159, 164 | orbi12d 916 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑢) = 𝑓 → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓))) |
166 | 165 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1st ‘𝑢) = 𝑓) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) ↔ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓))) |
167 | 142, 9 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom ((𝑀 Sat 𝐸)‘suc 𝑁) = (Fmla‘suc 𝑁)) |
168 | 167 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (Fmla‘suc 𝑁) = dom ((𝑀 Sat 𝐸)‘suc 𝑁)) |
169 | 168 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (Fmla‘suc 𝑁) ↔ 𝑔 ∈ dom ((𝑀 Sat 𝐸)‘suc 𝑁))) |
170 | | releldm2 7884 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (Rel
((𝑀 Sat 𝐸)‘suc 𝑁) → (𝑔 ∈ dom ((𝑀 Sat 𝐸)‘suc 𝑁) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1st ‘𝑣) = 𝑔)) |
171 | 80, 170 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ dom ((𝑀 Sat 𝐸)‘suc 𝑁) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1st ‘𝑣) = 𝑔)) |
172 | 169, 171 | bitrd 278 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (Fmla‘suc 𝑁) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1st ‘𝑣) = 𝑔)) |
173 | | r19.41v 3275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∃𝑣 ∈
((𝑀 Sat 𝐸)‘suc 𝑁)((1st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔𝑔)) ↔ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔𝑔))) |
174 | 1 | eqcomi 2747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑀 Sat 𝐸) = 𝑆 |
175 | 174 | fveq1i 6777 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑀 Sat 𝐸)‘suc 𝑁) = (𝑆‘suc 𝑁) |
176 | 175 | rexeqi 3346 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∃𝑣 ∈
((𝑀 Sat 𝐸)‘suc 𝑁)((1st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔𝑔)) ↔ ∃𝑣 ∈ (𝑆‘suc 𝑁)((1st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔𝑔))) |
177 | 89 | eqcoms 2746 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((1st ‘𝑣) = 𝑔 → ((1st ‘𝑢)⊼𝑔𝑔) = ((1st
‘𝑢)⊼𝑔(1st
‘𝑣))) |
178 | 177 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((1st ‘𝑣) = 𝑔 → (𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ↔ 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
179 | 178 | biimpa 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((1st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔𝑔)) → 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) |
180 | 179 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (((1st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔𝑔)) → 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
181 | 180 | reximdv 3201 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ (𝑆‘suc 𝑁)((1st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔𝑔)) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
182 | 176, 181 | syl5bi 241 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)((1st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔𝑔)) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
183 | 173, 182 | syl5bir 242 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1st ‘𝑣) = 𝑔 ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔𝑔)) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
184 | 183 | expd 416 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘suc 𝑁)(1st ‘𝑣) = 𝑔 → (𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))))) |
185 | 172, 184 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (Fmla‘suc 𝑁) → (𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))))) |
186 | 185 | rexlimdv 3211 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
187 | 186 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1st ‘𝑢) = 𝑓) → (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) → ∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
188 | 187 | orim1d 963 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1st ‘𝑢) = 𝑓) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
189 | 166, 188 | sylbird 259 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ω ∧ (𝑀 ∈
𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ (1st ‘𝑢) = 𝑓) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
190 | 189 | expimpd 454 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (((1st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓)) → (∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
191 | 190 | reximdva 3202 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))((1st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓)) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
192 | 156, 191 | syl5bir 242 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1st ‘𝑢) = 𝑓 ∧ (∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓)) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
193 | 192 | expd 416 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1st ‘𝑢) = 𝑓 → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) |
194 | 155, 193 | syl5bi 241 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑢) = 𝑓 → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) |
195 | 153, 194 | syld 47 |
. . . . . . . 8
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ((∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢))))) |
196 | 195 | rexlimdv 3211 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) → ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)))) |
197 | 145 | eleq2d 2824 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (Fmla‘𝑁) ↔ 𝑓 ∈ dom ((𝑀 Sat 𝐸)‘𝑁))) |
198 | 55, 100 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) → Rel ((𝑀 Sat 𝐸)‘𝑁)) |
199 | 198 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → Rel ((𝑀 Sat 𝐸)‘𝑁)) |
200 | | releldm2 7884 |
. . . . . . . . . . 11
⊢ (Rel
((𝑀 Sat 𝐸)‘𝑁) → (𝑓 ∈ dom ((𝑀 Sat 𝐸)‘𝑁) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1st ‘𝑢) = 𝑓)) |
201 | 199, 200 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ dom ((𝑀 Sat 𝐸)‘𝑁) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1st ‘𝑢) = 𝑓)) |
202 | 197, 201 | bitrd 278 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (Fmla‘𝑁) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1st ‘𝑢) = 𝑓)) |
203 | | r19.41v 3275 |
. . . . . . . . . . 11
⊢
(∃𝑢 ∈
((𝑀 Sat 𝐸)‘𝑁)((1st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔)) ↔ (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔))) |
204 | 42 | eqcomi 2747 |
. . . . . . . . . . . . 13
⊢ ((𝑀 Sat 𝐸)‘𝑁) = (𝑆‘𝑁) |
205 | 204 | rexeqi 3346 |
. . . . . . . . . . . 12
⊢
(∃𝑢 ∈
((𝑀 Sat 𝐸)‘𝑁)((1st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔)) ↔ ∃𝑢 ∈ (𝑆‘𝑁)((1st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔))) |
206 | 158 | rexbidv 3225 |
. . . . . . . . . . . . . . . 16
⊢
((1st ‘𝑢) = 𝑓 → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔))) |
207 | 206 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ (1st ‘𝑢) = 𝑓) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) ↔ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔))) |
208 | 146 | eleq2d 2824 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) ↔ 𝑔 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)))) |
209 | | releldmdifi 7886 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((Rel
((𝑀 Sat 𝐸)‘suc 𝑁) ∧ ((𝑀 Sat 𝐸)‘𝑁) ⊆ ((𝑀 Sat 𝐸)‘suc 𝑁)) → (𝑔 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) → ∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑣) = 𝑔)) |
210 | 80, 150, 209 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ (dom ((𝑀 Sat 𝐸)‘suc 𝑁) ∖ dom ((𝑀 Sat 𝐸)‘𝑁)) → ∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑣) = 𝑔)) |
211 | 208, 210 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → ∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑣) = 𝑔)) |
212 | 154 | rexeqi 3346 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑣 ∈
(((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑣) = 𝑔 ↔ ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1st ‘𝑣) = 𝑔) |
213 | 178 | biimpcd 248 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) → ((1st
‘𝑣) = 𝑔 → 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
214 | 213 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔𝑔)) → ((1st
‘𝑣) = 𝑔 → 𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
215 | 214 | reximdv 3201 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ 𝑥 = ((1st ‘𝑢)⊼𝑔𝑔)) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1st ‘𝑣) = 𝑔 → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
216 | 215 | ex 413 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1st ‘𝑣) = 𝑔 → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))))) |
217 | 216 | com23 86 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(1st ‘𝑣) = 𝑔 → (𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))))) |
218 | 212, 217 | syl5bi 241 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑣 ∈ (((𝑀 Sat 𝐸)‘suc 𝑁) ∖ ((𝑀 Sat 𝐸)‘𝑁))(1st ‘𝑣) = 𝑔 → (𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))))) |
219 | 211, 218 | syld 47 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁)) → (𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))))) |
220 | 219 | rexlimdv 3211 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
221 | 220 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ (1st ‘𝑢) = 𝑓) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
222 | 207, 221 | sylbird 259 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) ∧ (1st ‘𝑢) = 𝑓) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
223 | 222 | expimpd 454 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (((1st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔)) → ∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
224 | 223 | reximdv 3201 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (𝑆‘𝑁)((1st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔)) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
225 | 205, 224 | syl5bi 241 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)((1st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔)) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
226 | 203, 225 | syl5bir 242 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1st ‘𝑢) = 𝑓 ∧ ∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔)) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
227 | 226 | expd 416 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(1st ‘𝑢) = 𝑓 → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))))) |
228 | 202, 227 | sylbid 239 |
. . . . . . . 8
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (𝑓 ∈ (Fmla‘𝑁) → (∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))))) |
229 | 228 | rexlimdv 3211 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔) → ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
230 | 196, 229 | orim12d 962 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))))) |
231 | 141, 230 | impbid 211 |
. . . . 5
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣))) ↔
(∃𝑓 ∈
((Fmla‘suc 𝑁) ∖
(Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔)))) |
232 | 231 | abbidv 2807 |
. . . 4
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → {𝑥 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∨
∃𝑖 ∈ ω
𝑥 =
∀𝑔𝑖(1st ‘𝑢)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))} = {𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔))}) |
233 | 33, 232 | eqtrd 2778 |
. . 3
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → dom {〈𝑥, 𝑦〉 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴))} = {𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔))}) |
234 | 12, 233 | ineq12d 4149 |
. 2
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (dom (𝑆‘suc 𝑁) ∩ dom {〈𝑥, 𝑦〉 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴))}) = ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔))})) |
235 | | fmlasucdisj 33358 |
. . 3
⊢ (𝑁 ∈ ω →
((Fmla‘suc 𝑁) ∩
{𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔))}) = ∅) |
236 | 235 | ad2antrr 723 |
. 2
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → ((Fmla‘suc 𝑁) ∩ {𝑥 ∣ (∃𝑓 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))(∃𝑔 ∈ (Fmla‘suc 𝑁)𝑥 = (𝑓⊼𝑔𝑔) ∨ ∃𝑖 ∈ ω 𝑥 = ∀𝑔𝑖𝑓) ∨ ∃𝑓 ∈ (Fmla‘𝑁)∃𝑔 ∈ ((Fmla‘suc 𝑁) ∖ (Fmla‘𝑁))𝑥 = (𝑓⊼𝑔𝑔))}) = ∅) |
237 | 234, 236 | eqtrd 2778 |
1
⊢ (((𝑁 ∈ ω ∧ (𝑀 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊)) ∧ Fun (𝑆‘suc 𝑁)) → (dom (𝑆‘suc 𝑁) ∩ dom {〈𝑥, 𝑦〉 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴))}) = ∅) |