Step | Hyp | Ref
| Expression |
1 | | fveq2 6776 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑠 → (1st ‘𝑢) = (1st ‘𝑠)) |
2 | | fveq2 6776 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑟 → (1st ‘𝑣) = (1st ‘𝑟)) |
3 | 1, 2 | oveqan12d 7296 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
((1st ‘𝑠)⊼𝑔(1st
‘𝑟))) |
4 | 3 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔ 𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)))) |
5 | | fveq2 6776 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑠 → (2nd ‘𝑢) = (2nd ‘𝑠)) |
6 | | fveq2 6776 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑟 → (2nd ‘𝑣) = (2nd ‘𝑟)) |
7 | 5, 6 | ineqan12d 4150 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((2nd ‘𝑢) ∩ (2nd
‘𝑣)) =
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) |
8 | 7 | difeq2d 4058 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) |
9 | 8 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) ↔ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) |
10 | 4, 9 | anbi12d 631 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ↔ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))))) |
11 | 10 | cbvrexdva 3394 |
. . . . . . . . 9
⊢ (𝑢 = 𝑠 → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ↔ ∃𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))))) |
12 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗) |
13 | 1 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (1st ‘𝑢) = (1st ‘𝑠)) |
14 | 12, 13 | goaleq12d 33310 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → ∀𝑔𝑖(1st ‘𝑢) =
∀𝑔𝑗(1st ‘𝑠)) |
15 | 14 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ 𝑥 = ∀𝑔𝑗(1st ‘𝑠))) |
16 | | opeq1 4806 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑗 → 〈𝑖, 𝑘〉 = 〈𝑗, 𝑘〉) |
17 | 16 | sneqd 4575 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑗 → {〈𝑖, 𝑘〉} = {〈𝑗, 𝑘〉}) |
18 | | sneq 4573 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑗 → {𝑖} = {𝑗}) |
19 | 18 | difeq2d 4058 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑗 → (ω ∖ {𝑖}) = (ω ∖ {𝑗})) |
20 | 19 | reseq2d 5893 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = 𝑗 → (𝑓 ↾ (ω ∖ {𝑖})) = (𝑓 ↾ (ω ∖ {𝑗}))) |
21 | 17, 20 | uneq12d 4099 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = 𝑗 → ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) = ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗})))) |
22 | 21 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) = ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗})))) |
23 | 5 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (2nd ‘𝑢) = (2nd ‘𝑠)) |
24 | 22, 23 | eleq12d 2833 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢) ↔ ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠))) |
25 | 24 | ralbidv 3119 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢) ↔ ∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠))) |
26 | 25 | rabbidv 3413 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) |
27 | 26 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ↔ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)})) |
28 | 15, 27 | anbi12d 631 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) ↔ (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}))) |
29 | 28 | cbvrexdva 3394 |
. . . . . . . . 9
⊢ (𝑢 = 𝑠 → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) ↔ ∃𝑗 ∈ ω (𝑥 =
∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}))) |
30 | 11, 29 | orbi12d 916 |
. . . . . . . 8
⊢ (𝑢 = 𝑠 → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ (∃𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)})))) |
31 | 30 | cbvrexvw 3383 |
. . . . . . 7
⊢
(∃𝑢 ∈
((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ ∃𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}))) |
32 | | simp-4l 780 |
. . . . . . . . . . . . . . 15
⊢ (((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → Fun ((𝑀 Sat 𝐸)‘𝑁)) |
33 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) |
34 | 33 | anim1i 615 |
. . . . . . . . . . . . . . 15
⊢ (((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁))) |
35 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) |
36 | 35 | anim1i 615 |
. . . . . . . . . . . . . . . 16
⊢ (((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁))) |
37 | 36 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ (((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁))) |
38 | | satffunlem 33360 |
. . . . . . . . . . . . . . . . 17
⊢ (((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ (𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) → 𝑧 = 𝑦) |
39 | 38 | eqcomd 2744 |
. . . . . . . . . . . . . . . 16
⊢ (((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ (𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) → 𝑦 = 𝑧) |
40 | 39 | 3exp 1118 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ (𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁))) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑧))) |
41 | 32, 34, 37, 40 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ (((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑧))) |
42 | 41 | rexlimdva 3212 |
. . . . . . . . . . . . 13
⊢ ((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑧))) |
43 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 =
∀𝑔𝑖(1st ‘𝑢) → (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ↔
∀𝑔𝑖(1st ‘𝑢) = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)))) |
44 | | df-goal 33301 |
. . . . . . . . . . . . . . . . . . . 20
⊢
∀𝑔𝑖(1st ‘𝑢) = 〈2o, 〈𝑖, (1st ‘𝑢)〉〉 |
45 | | fvex 6789 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(1st ‘𝑠) ∈ V |
46 | | fvex 6789 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(1st ‘𝑟) ∈ V |
47 | | gonafv 33309 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘𝑠) ∈ V ∧ (1st ‘𝑟) ∈ V) →
((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) =
〈1o, 〈(1st ‘𝑠), (1st ‘𝑟)〉〉) |
48 | 45, 46, 47 | mp2an 689 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) =
〈1o, 〈(1st ‘𝑠), (1st ‘𝑟)〉〉 |
49 | 44, 48 | eqeq12i 2756 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑔𝑖(1st ‘𝑢) = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ↔
〈2o, 〈𝑖, (1st ‘𝑢)〉〉 = 〈1o,
〈(1st ‘𝑠), (1st ‘𝑟)〉〉) |
50 | | 2oex 8306 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
2o ∈ V |
51 | | opex 5381 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
〈𝑖,
(1st ‘𝑢)〉 ∈ V |
52 | 50, 51 | opth 5393 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈2o, 〈𝑖, (1st ‘𝑢)〉〉 = 〈1o,
〈(1st ‘𝑠), (1st ‘𝑟)〉〉 ↔ (2o =
1o ∧ 〈𝑖, (1st ‘𝑢)〉 = 〈(1st ‘𝑠), (1st ‘𝑟)〉)) |
53 | | 1one2o 8474 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
1o ≠ 2o |
54 | | df-ne 2944 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1o ≠ 2o ↔ ¬ 1o =
2o) |
55 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
1o = 2o → (1o = 2o →
(𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → 𝑦 = 𝑧))) |
56 | 54, 55 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(1o ≠ 2o → (1o = 2o
→ (𝑦 = ((𝑀 ↑m ω)
∖ ((2nd ‘𝑠) ∩ (2nd ‘𝑟))) → 𝑦 = 𝑧))) |
57 | 53, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(1o = 2o → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → 𝑦 = 𝑧)) |
58 | 57 | eqcoms 2746 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(2o = 1o → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → 𝑦 = 𝑧)) |
59 | 58 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((2o = 1o ∧ 〈𝑖, (1st ‘𝑢)〉 = 〈(1st ‘𝑠), (1st ‘𝑟)〉) → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → 𝑦 = 𝑧)) |
60 | 52, 59 | sylbi 216 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈2o, 〈𝑖, (1st ‘𝑢)〉〉 = 〈1o,
〈(1st ‘𝑠), (1st ‘𝑟)〉〉 → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → 𝑦 = 𝑧)) |
61 | 49, 60 | sylbi 216 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑔𝑖(1st ‘𝑢) = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → 𝑦 = 𝑧)) |
62 | 43, 61 | syl6bi 252 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 =
∀𝑔𝑖(1st ‘𝑢) → (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) → 𝑦 = 𝑧))) |
63 | 62 | impd 411 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 =
∀𝑔𝑖(1st ‘𝑢) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑧)) |
64 | 63 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 =
∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑧)) |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑧))) |
66 | 65 | rexlimdva 3212 |
. . . . . . . . . . . . 13
⊢ ((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑧))) |
67 | 42, 66 | jaod 856 |
. . . . . . . . . . . 12
⊢ ((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑧))) |
68 | 67 | rexlimdva 3212 |
. . . . . . . . . . 11
⊢ (((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑧))) |
69 | 68 | com23 86 |
. . . . . . . . . 10
⊢ (((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑦 = 𝑧))) |
70 | 69 | rexlimdva 3212 |
. . . . . . . . 9
⊢ ((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (∃𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑦 = 𝑧))) |
71 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 =
∀𝑔𝑗(1st ‘𝑠) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔
∀𝑔𝑗(1st ‘𝑠) = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
72 | | df-goal 33301 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
∀𝑔𝑗(1st ‘𝑠) = 〈2o, 〈𝑗, (1st ‘𝑠)〉〉 |
73 | | fvex 6789 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(1st ‘𝑢) ∈ V |
74 | | fvex 6789 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(1st ‘𝑣) ∈ V |
75 | | gonafv 33309 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘𝑢) ∈ V ∧ (1st ‘𝑣) ∈ V) →
((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
〈1o, 〈(1st ‘𝑢), (1st ‘𝑣)〉〉) |
76 | 73, 74, 75 | mp2an 689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
〈1o, 〈(1st ‘𝑢), (1st ‘𝑣)〉〉 |
77 | 72, 76 | eqeq12i 2756 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑔𝑗(1st ‘𝑠) = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔
〈2o, 〈𝑗, (1st ‘𝑠)〉〉 = 〈1o,
〈(1st ‘𝑢), (1st ‘𝑣)〉〉) |
78 | | opex 5381 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
〈𝑗,
(1st ‘𝑠)〉 ∈ V |
79 | 50, 78 | opth 5393 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(〈2o, 〈𝑗, (1st ‘𝑠)〉〉 = 〈1o,
〈(1st ‘𝑢), (1st ‘𝑣)〉〉 ↔ (2o =
1o ∧ 〈𝑗, (1st ‘𝑠)〉 = 〈(1st ‘𝑢), (1st ‘𝑣)〉)) |
80 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
1o = 2o → (1o = 2o →
𝑦 = 𝑧)) |
81 | 54, 80 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1o ≠ 2o → (1o = 2o
→ 𝑦 = 𝑧)) |
82 | 53, 81 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(1o = 2o → 𝑦 = 𝑧) |
83 | 82 | eqcoms 2746 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(2o = 1o → 𝑦 = 𝑧) |
84 | 83 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((2o = 1o ∧ 〈𝑗, (1st ‘𝑠)〉 = 〈(1st ‘𝑢), (1st ‘𝑣)〉) → 𝑦 = 𝑧) |
85 | 79, 84 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈2o, 〈𝑗, (1st ‘𝑠)〉〉 = 〈1o,
〈(1st ‘𝑢), (1st ‘𝑣)〉〉 → 𝑦 = 𝑧) |
86 | 77, 85 | sylbi 216 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑔𝑗(1st ‘𝑠) = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) → 𝑦 = 𝑧) |
87 | 71, 86 | syl6bi 252 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 =
∀𝑔𝑗(1st ‘𝑠) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) → 𝑦 = 𝑧)) |
88 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 =
∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) → 𝑦 = 𝑧)) |
89 | 88 | com12 32 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) → ((𝑥 =
∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑧)) |
90 | 89 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑧)) |
91 | 90 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑧))) |
92 | 91 | rexlimdva 3212 |
. . . . . . . . . . . . 13
⊢ ((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑧))) |
93 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 =
∀𝑔𝑖(1st ‘𝑢) → (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ↔
∀𝑔𝑖(1st ‘𝑢) = ∀𝑔𝑗(1st ‘𝑠))) |
94 | 44, 72 | eqeq12i 2756 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑔𝑖(1st ‘𝑢) = ∀𝑔𝑗(1st ‘𝑠) ↔ 〈2o,
〈𝑖, (1st
‘𝑢)〉〉 =
〈2o, 〈𝑗, (1st ‘𝑠)〉〉) |
95 | 50, 51 | opth 5393 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(〈2o, 〈𝑖, (1st ‘𝑢)〉〉 = 〈2o,
〈𝑗, (1st
‘𝑠)〉〉
↔ (2o = 2o ∧ 〈𝑖, (1st ‘𝑢)〉 = 〈𝑗, (1st ‘𝑠)〉)) |
96 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑖 ∈ V |
97 | 96, 73 | opth 5393 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑖,
(1st ‘𝑢)〉 = 〈𝑗, (1st ‘𝑠)〉 ↔ (𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠))) |
98 | 97 | anbi2i 623 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((2o = 2o ∧ 〈𝑖, (1st ‘𝑢)〉 = 〈𝑗, (1st ‘𝑠)〉) ↔ (2o =
2o ∧ (𝑖 =
𝑗 ∧ (1st
‘𝑢) = (1st
‘𝑠)))) |
99 | 94, 95, 98 | 3bitri 297 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑔𝑖(1st ‘𝑢) = ∀𝑔𝑗(1st ‘𝑠) ↔ (2o =
2o ∧ (𝑖 =
𝑗 ∧ (1st
‘𝑢) = (1st
‘𝑠)))) |
100 | 93, 99 | bitrdi 287 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 =
∀𝑔𝑖(1st ‘𝑢) → (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ↔ (2o =
2o ∧ (𝑖 =
𝑗 ∧ (1st
‘𝑢) = (1st
‘𝑠))))) |
101 | 100 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) → (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ↔ (2o =
2o ∧ (𝑖 =
𝑗 ∧ (1st
‘𝑢) = (1st
‘𝑠))))) |
102 | | funfv1st2nd 7887 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠)) |
103 | 102 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Fun
((𝑀 Sat 𝐸)‘𝑁) → (𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁) → (((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠))) |
104 | | funfv1st2nd 7887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢)) |
105 | 104 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (Fun
((𝑀 Sat 𝐸)‘𝑁) → (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) → (((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢))) |
106 | | fveqeq2 6785 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((1st ‘𝑢) = (1st ‘𝑠) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢) ↔ (((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑢))) |
107 | | eqtr2 2762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑢) ∧ (((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠)) →
(2nd ‘𝑢) =
(2nd ‘𝑠)) |
108 | | opeq1 4806 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑗 = 𝑖 → 〈𝑗, 𝑘〉 = 〈𝑖, 𝑘〉) |
109 | 108 | sneqd 4575 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑗 = 𝑖 → {〈𝑗, 𝑘〉} = {〈𝑖, 𝑘〉}) |
110 | | sneq 4573 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑗 = 𝑖 → {𝑗} = {𝑖}) |
111 | 110 | difeq2d 4058 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑗 = 𝑖 → (ω ∖ {𝑗}) = (ω ∖ {𝑖})) |
112 | 111 | reseq2d 5893 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑗 = 𝑖 → (𝑓 ↾ (ω ∖ {𝑗})) = (𝑓 ↾ (ω ∖ {𝑖}))) |
113 | 109, 112 | uneq12d 4099 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑗 = 𝑖 → ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) = ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖})))) |
114 | 113 | eqcoms 2746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑖 = 𝑗 → ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) = ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖})))) |
115 | 114 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) = ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖})))) |
116 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → (2nd ‘𝑢) = (2nd ‘𝑠)) |
117 | 116 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → (2nd ‘𝑠) = (2nd ‘𝑢)) |
118 | 115, 117 | eleq12d 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → (({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠) ↔ ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢))) |
119 | 118 | ralbidv 3119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → (∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠) ↔ ∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢))) |
120 | 119 | rabbidv 3413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) |
121 | | eqeq12 2755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → (𝑦 = 𝑧 ↔ {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) |
122 | 120, 121 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → ((𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → 𝑦 = 𝑧)) |
123 | 122 | exp4b 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((2nd ‘𝑢) = (2nd ‘𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧)))) |
124 | 107, 123 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑢) ∧ (((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠)) → (𝑖 = 𝑗 → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧)))) |
125 | 124 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑢) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧))))) |
126 | 106, 125 | syl6bi 252 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((1st ‘𝑢) = (1st ‘𝑠) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧)))))) |
127 | 126 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((1st ‘𝑢) = (1st ‘𝑠) → (𝑖 = 𝑗 → ((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢) → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧)))))) |
128 | 127 | impcom 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢) → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧))))) |
129 | 128 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠) → ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧))))) |
130 | 105, 129 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (Fun
((𝑀 Sat 𝐸)‘𝑁) → (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠) → ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧)))))) |
131 | 130 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Fun
((𝑀 Sat 𝐸)‘𝑁) → ((((𝑀 Sat 𝐸)‘𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠) → (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) → ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧)))))) |
132 | 103, 131 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (Fun
((𝑀 Sat 𝐸)‘𝑁) → (𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁) → (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) → ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧)))))) |
133 | 132 | imp 407 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) → ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧))))) |
134 | 133 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) → (𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁) → ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧))))) |
135 | 134 | imp 407 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧)))) |
136 | 135 | adantld 491 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → ((2o = 2o
∧ (𝑖 = 𝑗 ∧ (1st
‘𝑢) = (1st
‘𝑠))) → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧)))) |
137 | 136 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) → ((2o =
2o ∧ (𝑖 =
𝑗 ∧ (1st
‘𝑢) = (1st
‘𝑠))) → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧)))) |
138 | 101, 137 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) → (𝑥 = ∀𝑔𝑗(1st ‘𝑠) → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧)))) |
139 | 138 | impd 411 |
. . . . . . . . . . . . . . . . 17
⊢ ((((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧))) |
140 | 139 | ex 413 |
. . . . . . . . . . . . . . . 16
⊢ (((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → 𝑦 = 𝑧)))) |
141 | 140 | com34 91 |
. . . . . . . . . . . . . . 15
⊢ (((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) → (𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑧)))) |
142 | 141 | impd 411 |
. . . . . . . . . . . . . 14
⊢ (((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑖 ∈ ω) → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑧))) |
143 | 142 | rexlimdva 3212 |
. . . . . . . . . . . . 13
⊢ ((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑧))) |
144 | 92, 143 | jaod 856 |
. . . . . . . . . . . 12
⊢ ((((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑧))) |
145 | 144 | rexlimdva 3212 |
. . . . . . . . . . 11
⊢ (((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑧))) |
146 | 145 | com23 86 |
. . . . . . . . . 10
⊢ (((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) ∧ 𝑗 ∈ ω) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑦 = 𝑧))) |
147 | 146 | rexlimdva 3212 |
. . . . . . . . 9
⊢ ((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → (∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑦 = 𝑧))) |
148 | 70, 147 | jaod 856 |
. . . . . . . 8
⊢ ((Fun
((𝑀 Sat 𝐸)‘𝑁) ∧ 𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)) → ((∃𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)})) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑦 = 𝑧))) |
149 | 148 | rexlimdva 3212 |
. . . . . . 7
⊢ (Fun
((𝑀 Sat 𝐸)‘𝑁) → (∃𝑠 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑟 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑗, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)})) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑦 = 𝑧))) |
150 | 31, 149 | syl5bi 241 |
. . . . . 6
⊢ (Fun
((𝑀 Sat 𝐸)‘𝑁) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) → 𝑦 = 𝑧))) |
151 | 150 | impd 411 |
. . . . 5
⊢ (Fun
((𝑀 Sat 𝐸)‘𝑁) → ((∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ∧ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) → 𝑦 = 𝑧)) |
152 | 151 | alrimivv 1931 |
. . . 4
⊢ (Fun
((𝑀 Sat 𝐸)‘𝑁) → ∀𝑦∀𝑧((∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ∧ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) → 𝑦 = 𝑧)) |
153 | | eqeq1 2742 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) ↔ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))))) |
154 | 153 | anbi2d 629 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ↔ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))))) |
155 | 154 | rexbidv 3225 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ↔ ∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))))) |
156 | | eqeq1 2742 |
. . . . . . . . 9
⊢ (𝑦 = 𝑧 → (𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ↔ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) |
157 | 156 | anbi2d 629 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) ↔ (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) |
158 | 157 | rexbidv 3225 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) ↔ ∃𝑖 ∈ ω (𝑥 =
∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) |
159 | 155, 158 | orbi12d 916 |
. . . . . 6
⊢ (𝑦 = 𝑧 → ((∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ (∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))) |
160 | 159 | rexbidv 3225 |
. . . . 5
⊢ (𝑦 = 𝑧 → (∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})))) |
161 | 160 | mo4 2566 |
. . . 4
⊢
(∃*𝑦∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ↔ ∀𝑦∀𝑧((∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)})) ∧ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑧 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑧 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) → 𝑦 = 𝑧)) |
162 | 152, 161 | sylibr 233 |
. . 3
⊢ (Fun
((𝑀 Sat 𝐸)‘𝑁) → ∃*𝑦∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) |
163 | 162 | alrimiv 1930 |
. 2
⊢ (Fun
((𝑀 Sat 𝐸)‘𝑁) → ∀𝑥∃*𝑦∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) |
164 | | funopab 6471 |
. 2
⊢ (Fun
{〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))} ↔ ∀𝑥∃*𝑦∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))) |
165 | 163, 164 | sylibr 233 |
1
⊢ (Fun
((𝑀 Sat 𝐸)‘𝑁) → Fun {〈𝑥, 𝑦〉 ∣ ∃𝑢 ∈ ((𝑀 Sat 𝐸)‘𝑁)(∃𝑣 ∈ ((𝑀 Sat 𝐸)‘𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = {𝑓 ∈ (𝑀 ↑m ω) ∣
∀𝑘 ∈ 𝑀 ({〈𝑖, 𝑘〉} ∪ (𝑓 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}))}) |