Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → 𝑢 = 𝑠) |
2 | 1 | fveq2d 6739 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (1st ‘𝑢) = (1st ‘𝑠)) |
3 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → 𝑣 = 𝑟) |
4 | 3 | fveq2d 6739 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (1st ‘𝑣) = (1st ‘𝑟)) |
5 | 2, 4 | oveq12d 7249 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
((1st ‘𝑠)⊼𝑔(1st
‘𝑟))) |
6 | 5 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔ 𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)))) |
7 | | satffunlem2lem1.a |
. . . . . . . . . . . . . 14
⊢ 𝐴 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) |
8 | 1 | fveq2d 6739 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (2nd ‘𝑢) = (2nd ‘𝑠)) |
9 | 3 | fveq2d 6739 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (2nd ‘𝑣) = (2nd ‘𝑟)) |
10 | 8, 9 | ineq12d 4142 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((2nd ‘𝑢) ∩ (2nd
‘𝑣)) =
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) |
11 | 10 | difeq2d 4051 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) |
12 | 7, 11 | syl5eq 2791 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → 𝐴 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) |
13 | 12 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (𝑦 = 𝐴 ↔ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) |
14 | 6, 13 | anbi12d 634 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))))) |
15 | 14 | cbvrexdva 3382 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑠 → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))))) |
16 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗) |
17 | | fveq2 6735 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑠 → (1st ‘𝑢) = (1st ‘𝑠)) |
18 | 17 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (1st ‘𝑢) = (1st ‘𝑠)) |
19 | 16, 18 | goaleq12d 33049 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → ∀𝑔𝑖(1st ‘𝑢) =
∀𝑔𝑗(1st ‘𝑠)) |
20 | 19 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ↔ 𝑥 = ∀𝑔𝑗(1st ‘𝑠))) |
21 | | satffunlem2lem1.b |
. . . . . . . . . . . . . 14
⊢ 𝐵 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} |
22 | 21 | eqeq2i 2751 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝐵 ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) |
23 | | opeq1 4798 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑗 → 〈𝑖, 𝑧〉 = 〈𝑗, 𝑧〉) |
24 | 23 | sneqd 4567 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑗 → {〈𝑖, 𝑧〉} = {〈𝑗, 𝑧〉}) |
25 | | sneq 4565 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑗 → {𝑖} = {𝑗}) |
26 | 25 | difeq2d 4051 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑗 → (ω ∖ {𝑖}) = (ω ∖ {𝑗})) |
27 | 26 | reseq2d 5865 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑗 → (𝑎 ↾ (ω ∖ {𝑖})) = (𝑎 ↾ (ω ∖ {𝑗}))) |
28 | 24, 27 | uneq12d 4092 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = 𝑗 → ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) = ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗})))) |
29 | 28 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) = ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗})))) |
30 | | fveq2 6735 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑠 → (2nd ‘𝑢) = (2nd ‘𝑠)) |
31 | 30 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (2nd ‘𝑢) = (2nd ‘𝑠)) |
32 | 29, 31 | eleq12d 2833 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢) ↔ ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠))) |
33 | 32 | ralbidv 3119 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢) ↔ ∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠))) |
34 | 33 | rabbidv 3402 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) |
35 | 34 | eqeq2d 2749 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)} ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)})) |
36 | 22, 35 | syl5bb 286 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → (𝑦 = 𝐵 ↔ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)})) |
37 | 20, 36 | anbi12d 634 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑠 ∧ 𝑖 = 𝑗) → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵) ↔ (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}))) |
38 | 37 | cbvrexdva 3382 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑠 → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵) ↔ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}))) |
39 | 15, 38 | orbi12d 919 |
. . . . . . . . 9
⊢ (𝑢 = 𝑠 → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)})))) |
40 | 39 | cbvrexvw 3371 |
. . . . . . . 8
⊢
(∃𝑢 ∈
((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}))) |
41 | | fveq2 6735 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑟 → (1st ‘𝑣) = (1st ‘𝑟)) |
42 | 17, 41 | oveqan12d 7250 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
((1st ‘𝑠)⊼𝑔(1st
‘𝑟))) |
43 | 42 | eqeq2d 2749 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔ 𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)))) |
44 | 7 | eqeq2i 2751 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝐴 ↔ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) |
45 | | fveq2 6735 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑟 → (2nd ‘𝑣) = (2nd ‘𝑟)) |
46 | 30, 45 | ineqan12d 4143 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((2nd ‘𝑢) ∩ (2nd
‘𝑣)) =
((2nd ‘𝑠)
∩ (2nd ‘𝑟))) |
47 | 46 | difeq2d 4051 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) |
48 | 47 | eqeq2d 2749 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))) ↔ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) |
49 | 44, 48 | syl5bb 286 |
. . . . . . . . . . 11
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → (𝑦 = 𝐴 ↔ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) |
50 | 43, 49 | anbi12d 634 |
. . . . . . . . . 10
⊢ ((𝑢 = 𝑠 ∧ 𝑣 = 𝑟) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))))) |
51 | 50 | cbvrexdva 3382 |
. . . . . . . . 9
⊢ (𝑢 = 𝑠 → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))))) |
52 | 51 | cbvrexvw 3371 |
. . . . . . . 8
⊢
(∃𝑢 ∈
(𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑠 ∈ (𝑆‘𝑁)∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) |
53 | 40, 52 | orbi12i 915 |
. . . . . . 7
⊢
((∃𝑢 ∈
((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴)) ↔ (∃𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)})) ∨ ∃𝑠 ∈ (𝑆‘𝑁)∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))))) |
54 | | simp-5l 785 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → Fun (𝑆‘suc 𝑁)) |
55 | | eldifi 4055 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → 𝑠 ∈ (𝑆‘suc 𝑁)) |
56 | 55 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → 𝑠 ∈ (𝑆‘suc 𝑁)) |
57 | 56 | anim1i 618 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁))) |
58 | 57 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁))) |
59 | | eldifi 4055 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → 𝑢 ∈ (𝑆‘suc 𝑁)) |
60 | 59 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → 𝑢 ∈ (𝑆‘suc 𝑁)) |
61 | 60 | anim1i 618 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) |
62 | 54, 58, 61 | 3jca 1130 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))) |
63 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) |
64 | 7 | eqeq2i 2751 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝐴 ↔ 𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) |
65 | 64 | biimpi 219 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝐴 → 𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣)))) |
66 | 65 | anim2i 620 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))))) |
67 | | satffunlem 33099 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((Fun
(𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))))) → 𝑦 = 𝑤) |
68 | 62, 63, 66, 67 | syl3an 1162 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤) |
69 | 68 | 3exp 1121 |
. . . . . . . . . . . . . . . . 17
⊢ ((((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤))) |
70 | 69 | com23 86 |
. . . . . . . . . . . . . . . 16
⊢ ((((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑤))) |
71 | 70 | rexlimdva 3211 |
. . . . . . . . . . . . . . 15
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑤))) |
72 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) → (𝑥 =
∀𝑔𝑖(1st ‘𝑢) ↔ ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) =
∀𝑔𝑖(1st ‘𝑢))) |
73 | | fvex 6748 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1st ‘𝑠) ∈ V |
74 | | fvex 6748 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1st ‘𝑟) ∈ V |
75 | | gonafv 33048 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((1st ‘𝑠) ∈ V ∧ (1st ‘𝑟) ∈ V) →
((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) =
〈1o, 〈(1st ‘𝑠), (1st ‘𝑟)〉〉) |
76 | 73, 74, 75 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) =
〈1o, 〈(1st ‘𝑠), (1st ‘𝑟)〉〉 |
77 | | df-goal 33040 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
∀𝑔𝑖(1st ‘𝑢) = 〈2o, 〈𝑖, (1st ‘𝑢)〉〉 |
78 | 76, 77 | eqeq12i 2756 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) =
∀𝑔𝑖(1st ‘𝑢) ↔ 〈1o,
〈(1st ‘𝑠), (1st ‘𝑟)〉〉 = 〈2o,
〈𝑖, (1st
‘𝑢)〉〉) |
79 | | 1oex 8235 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
1o ∈ V |
80 | | opex 5362 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
〈(1st ‘𝑠), (1st ‘𝑟)〉 ∈ V |
81 | 79, 80 | opth 5374 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈1o, 〈(1st ‘𝑠), (1st ‘𝑟)〉〉 = 〈2o,
〈𝑖, (1st
‘𝑢)〉〉
↔ (1o = 2o ∧ 〈(1st ‘𝑠), (1st ‘𝑟)〉 = 〈𝑖, (1st ‘𝑢)〉)) |
82 | | 1one2o 8391 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
1o ≠ 2o |
83 | | df-ne 2942 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(1o ≠ 2o ↔ ¬ 1o =
2o) |
84 | | pm2.21 123 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (¬
1o = 2o → (1o = 2o →
𝑦 = 𝑤)) |
85 | 83, 84 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(1o ≠ 2o → (1o = 2o
→ 𝑦 = 𝑤)) |
86 | 82, 85 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1o = 2o → 𝑦 = 𝑤) |
87 | 86 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((1o = 2o ∧ 〈(1st ‘𝑠), (1st ‘𝑟)〉 = 〈𝑖, (1st ‘𝑢)〉) → 𝑦 = 𝑤) |
88 | 81, 87 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(〈1o, 〈(1st ‘𝑠), (1st ‘𝑟)〉〉 = 〈2o,
〈𝑖, (1st
‘𝑢)〉〉
→ 𝑦 = 𝑤) |
89 | 78, 88 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) =
∀𝑔𝑖(1st ‘𝑢) → 𝑦 = 𝑤) |
90 | 72, 89 | syl6bi 256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) → (𝑥 =
∀𝑔𝑖(1st ‘𝑢) → 𝑦 = 𝑤)) |
91 | 90 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) → 𝑦 = 𝑤)) |
92 | 91 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 =
∀𝑔𝑖(1st ‘𝑢) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑤)) |
93 | 92 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 =
∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑤)) |
94 | 93 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑤))) |
95 | 94 | rexlimdva 3211 |
. . . . . . . . . . . . . . 15
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑤))) |
96 | 71, 95 | jaod 859 |
. . . . . . . . . . . . . 14
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑤))) |
97 | 96 | rexlimdva 3211 |
. . . . . . . . . . . . 13
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑤))) |
98 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . 18
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → Fun (𝑆‘suc 𝑁)) |
99 | 57 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁))) |
100 | | ssel 3907 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁) → (𝑢 ∈ (𝑆‘𝑁) → 𝑢 ∈ (𝑆‘suc 𝑁))) |
101 | 100 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘𝑁) → 𝑢 ∈ (𝑆‘suc 𝑁))) |
102 | 101 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ (𝑆‘𝑁) → ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → 𝑢 ∈ (𝑆‘suc 𝑁))) |
103 | 102 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → 𝑢 ∈ (𝑆‘suc 𝑁))) |
104 | 103 | impcom 411 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑢 ∈ (𝑆‘suc 𝑁)) |
105 | | eldifi 4055 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → 𝑣 ∈ (𝑆‘suc 𝑁)) |
106 | 105 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑣 ∈ (𝑆‘suc 𝑁)) |
107 | 104, 106 | jca 515 |
. . . . . . . . . . . . . . . . . 18
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) |
108 | 98, 99, 107 | 3jca 1130 |
. . . . . . . . . . . . . . . . 17
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))) |
109 | 108, 63, 66, 67 | syl3an 1162 |
. . . . . . . . . . . . . . . 16
⊢ ((((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤) |
110 | 109 | 3exp 1121 |
. . . . . . . . . . . . . . 15
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤))) |
111 | 110 | com23 86 |
. . . . . . . . . . . . . 14
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑤))) |
112 | 111 | rexlimdvva 3221 |
. . . . . . . . . . . . 13
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → (∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑤))) |
113 | 97, 112 | jaod 859 |
. . . . . . . . . . . 12
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → 𝑦 = 𝑤))) |
114 | 113 | com23 86 |
. . . . . . . . . . 11
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤))) |
115 | 114 | rexlimdva 3211 |
. . . . . . . . . 10
⊢ (((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤))) |
116 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 =
∀𝑔𝑗(1st ‘𝑠) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔
∀𝑔𝑗(1st ‘𝑠) = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)))) |
117 | | df-goal 33040 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
∀𝑔𝑗(1st ‘𝑠) = 〈2o, 〈𝑗, (1st ‘𝑠)〉〉 |
118 | | fvex 6748 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1st ‘𝑢) ∈ V |
119 | | fvex 6748 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1st ‘𝑣) ∈ V |
120 | | gonafv 33048 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((1st ‘𝑢) ∈ V ∧ (1st ‘𝑣) ∈ V) →
((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
〈1o, 〈(1st ‘𝑢), (1st ‘𝑣)〉〉) |
121 | 118, 119,
120 | mp2an 692 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) =
〈1o, 〈(1st ‘𝑢), (1st ‘𝑣)〉〉 |
122 | 117, 121 | eqeq12i 2756 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑔𝑗(1st ‘𝑠) = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ↔
〈2o, 〈𝑗, (1st ‘𝑠)〉〉 = 〈1o,
〈(1st ‘𝑢), (1st ‘𝑣)〉〉) |
123 | | 2oex 8239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
2o ∈ V |
124 | | opex 5362 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
〈𝑗,
(1st ‘𝑠)〉 ∈ V |
125 | 123, 124 | opth 5374 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈2o, 〈𝑗, (1st ‘𝑠)〉〉 = 〈1o,
〈(1st ‘𝑢), (1st ‘𝑣)〉〉 ↔ (2o =
1o ∧ 〈𝑗, (1st ‘𝑠)〉 = 〈(1st ‘𝑢), (1st ‘𝑣)〉)) |
126 | 86 | eqcoms 2746 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(2o = 1o → 𝑦 = 𝑤) |
127 | 126 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((2o = 1o ∧ 〈𝑗, (1st ‘𝑠)〉 = 〈(1st ‘𝑢), (1st ‘𝑣)〉) → 𝑦 = 𝑤) |
128 | 125, 127 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(〈2o, 〈𝑗, (1st ‘𝑠)〉〉 = 〈1o,
〈(1st ‘𝑢), (1st ‘𝑣)〉〉 → 𝑦 = 𝑤) |
129 | 122, 128 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑔𝑗(1st ‘𝑠) = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) → 𝑦 = 𝑤) |
130 | 116, 129 | syl6bi 256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 =
∀𝑔𝑗(1st ‘𝑠) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) → 𝑦 = 𝑤)) |
131 | 130 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 =
∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) → 𝑦 = 𝑤)) |
132 | 131 | com12 32 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) → ((𝑥 =
∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑤)) |
133 | 132 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑤)) |
134 | 133 | rexlimivw 3209 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑣 ∈
(𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑤)) |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑤))) |
136 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 =
∀𝑔𝑖(1st ‘𝑢) → (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ↔
∀𝑔𝑖(1st ‘𝑢) = ∀𝑔𝑗(1st ‘𝑠))) |
137 | 77, 117 | eqeq12i 2756 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(∀𝑔𝑖(1st ‘𝑢) = ∀𝑔𝑗(1st ‘𝑠) ↔ 〈2o,
〈𝑖, (1st
‘𝑢)〉〉 =
〈2o, 〈𝑗, (1st ‘𝑠)〉〉) |
138 | | opex 5362 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
〈𝑖,
(1st ‘𝑢)〉 ∈ V |
139 | 123, 138 | opth 5374 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈2o, 〈𝑖, (1st ‘𝑢)〉〉 = 〈2o,
〈𝑗, (1st
‘𝑠)〉〉
↔ (2o = 2o ∧ 〈𝑖, (1st ‘𝑢)〉 = 〈𝑗, (1st ‘𝑠)〉)) |
140 | | vex 3424 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑖 ∈ V |
141 | 140, 118 | opth 5374 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(〈𝑖,
(1st ‘𝑢)〉 = 〈𝑗, (1st ‘𝑠)〉 ↔ (𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠))) |
142 | 141 | anbi2i 626 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((2o = 2o ∧ 〈𝑖, (1st ‘𝑢)〉 = 〈𝑗, (1st ‘𝑠)〉) ↔ (2o =
2o ∧ (𝑖 =
𝑗 ∧ (1st
‘𝑢) = (1st
‘𝑠)))) |
143 | 137, 139,
142 | 3bitri 300 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(∀𝑔𝑖(1st ‘𝑢) = ∀𝑔𝑗(1st ‘𝑠) ↔ (2o =
2o ∧ (𝑖 =
𝑗 ∧ (1st
‘𝑢) = (1st
‘𝑠)))) |
144 | 136, 143 | bitrdi 290 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 =
∀𝑔𝑖(1st ‘𝑢) → (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ↔ (2o =
2o ∧ (𝑖 =
𝑗 ∧ (1st
‘𝑢) = (1st
‘𝑠))))) |
145 | 144 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) → (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ↔ (2o =
2o ∧ (𝑖 =
𝑗 ∧ (1st
‘𝑢) = (1st
‘𝑠))))) |
146 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → 𝑠 ∈ (𝑆‘suc 𝑁))) |
147 | | funfv1st2nd 7835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ 𝑠 ∈ (𝑆‘suc 𝑁)) → ((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠)) |
148 | 147 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Fun
(𝑆‘suc 𝑁) → (𝑠 ∈ (𝑆‘suc 𝑁) → ((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠))) |
149 | 148 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑠 ∈ (𝑆‘suc 𝑁) → ((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠))) |
150 | | funfv1st2nd 7835 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ 𝑢 ∈ (𝑆‘suc 𝑁)) → ((𝑆‘suc 𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢)) |
151 | 150 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (Fun
(𝑆‘suc 𝑁) → (𝑢 ∈ (𝑆‘suc 𝑁) → ((𝑆‘suc 𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢))) |
152 | 151 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘suc 𝑁) → ((𝑆‘suc 𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢))) |
153 | | fveqeq2 6744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
((1st ‘𝑢) = (1st ‘𝑠) → (((𝑆‘suc 𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢) ↔ ((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑢))) |
154 | | eqtr2 2762 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑢) ∧ ((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠)) →
(2nd ‘𝑢) =
(2nd ‘𝑠)) |
155 | 28 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑖 = 𝑗 → ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) = ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖})))) |
156 | 155 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) = ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖})))) |
157 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → (2nd ‘𝑢) = (2nd ‘𝑠)) |
158 | 157 | eqcomd 2744 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → (2nd ‘𝑠) = (2nd ‘𝑢)) |
159 | 156, 158 | eleq12d 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → (({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠) ↔ ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢))) |
160 | 159 | ralbidv 3119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → (∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠) ↔ ∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢))) |
161 | 160 | rabbidv 3402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑖, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑖}))) ∈ (2nd ‘𝑢)}) |
162 | 161, 21 | eqtr4di 2797 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} = 𝐵) |
163 | | eqeq12 2755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} ∧ 𝑤 = 𝐵) → (𝑦 = 𝑤 ↔ {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} = 𝐵)) |
164 | 162, 163 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((2nd ‘𝑢) = (2nd ‘𝑠) ∧ 𝑖 = 𝑗) → ((𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤)) |
165 | 164 | exp4b 434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
((2nd ‘𝑢) = (2nd ‘𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))) |
166 | 154, 165 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑢) ∧ ((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠)) → (𝑖 = 𝑗 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))) |
167 | 166 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑢) → (((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))) |
168 | 153, 167 | syl6bi 256 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
((1st ‘𝑢) = (1st ‘𝑠) → (((𝑆‘suc 𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢) → (((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠) → (𝑖 = 𝑗 → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))))) |
169 | 168 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
((1st ‘𝑢) = (1st ‘𝑠) → (𝑖 = 𝑗 → (((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠) → (((𝑆‘suc 𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))))) |
170 | 169 | impcom 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠) → (((𝑆‘suc 𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))) |
171 | 170 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑆‘suc 𝑁)‘(1st ‘𝑢)) = (2nd
‘𝑢) → (((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠) → ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))) |
172 | 59, 152, 171 | syl56 36 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠) → ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))))) |
173 | 172 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (((𝑆‘suc 𝑁)‘(1st ‘𝑠)) = (2nd
‘𝑠) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))))) |
174 | 146, 149,
173 | 3syld 60 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))))) |
175 | 174 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))) |
176 | 175 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) → (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤))))) |
177 | 176 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((𝑖 = 𝑗 ∧ (1st ‘𝑢) = (1st ‘𝑠)) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))) |
178 | 177 | adantld 494 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((2o = 2o
∧ (𝑖 = 𝑗 ∧ (1st
‘𝑢) = (1st
‘𝑠))) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))) |
179 | 178 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) → ((2o =
2o ∧ (𝑖 =
𝑗 ∧ (1st
‘𝑢) = (1st
‘𝑠))) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))) |
180 | 145, 179 | sylbid 243 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) → (𝑥 = ∀𝑔𝑗(1st ‘𝑠) → (𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)} → (𝑤 = 𝐵 → 𝑦 = 𝑤)))) |
181 | 180 | impd 414 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) ∧ 𝑥 = ∀𝑔𝑖(1st ‘𝑢)) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → (𝑤 = 𝐵 → 𝑦 = 𝑤))) |
182 | 181 | ex 416 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → (𝑤 = 𝐵 → 𝑦 = 𝑤)))) |
183 | 182 | com34 91 |
. . . . . . . . . . . . . . . . 17
⊢ ((((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) → (𝑥 = ∀𝑔𝑖(1st ‘𝑢) → (𝑤 = 𝐵 → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑤)))) |
184 | 183 | impd 414 |
. . . . . . . . . . . . . . . 16
⊢ ((((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑤))) |
185 | 184 | rexlimdva 3211 |
. . . . . . . . . . . . . . 15
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑤))) |
186 | 135, 185 | jaod 859 |
. . . . . . . . . . . . . 14
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑤))) |
187 | 186 | rexlimdva 3211 |
. . . . . . . . . . . . 13
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑤))) |
188 | 133 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ (𝑆‘𝑁)) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑤))) |
189 | 188 | rexlimdva 3211 |
. . . . . . . . . . . . . 14
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) ∧ 𝑢 ∈ (𝑆‘𝑁)) → (∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑤))) |
190 | 189 | rexlimdva 3211 |
. . . . . . . . . . . . 13
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) → (∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑤))) |
191 | 187, 190 | jaod 859 |
. . . . . . . . . . . 12
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → 𝑦 = 𝑤))) |
192 | 191 | com23 86 |
. . . . . . . . . . 11
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑗 ∈ ω) → ((𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤))) |
193 | 192 | rexlimdva 3211 |
. . . . . . . . . 10
⊢ (((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)}) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤))) |
194 | 115, 193 | jaod 859 |
. . . . . . . . 9
⊢ (((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ 𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)})) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤))) |
195 | 194 | rexlimdva 3211 |
. . . . . . . 8
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (∃𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)})) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤))) |
196 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → Fun (𝑆‘suc 𝑁)) |
197 | | ssel 3907 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁) → (𝑠 ∈ (𝑆‘𝑁) → 𝑠 ∈ (𝑆‘suc 𝑁))) |
198 | 197 | adantrd 495 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁) → ((𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → 𝑠 ∈ (𝑆‘suc 𝑁))) |
199 | 198 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → ((𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → 𝑠 ∈ (𝑆‘suc 𝑁))) |
200 | 199 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑠 ∈ (𝑆‘suc 𝑁)) |
201 | | eldifi 4055 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) → 𝑟 ∈ (𝑆‘suc 𝑁)) |
202 | 201 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑟 ∈ (𝑆‘suc 𝑁)) |
203 | 200, 202 | jca 515 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁))) |
204 | 203 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁))) |
205 | 59 | anim1i 618 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) |
206 | 205 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) |
207 | 196, 204,
206 | 3jca 1130 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))) |
208 | 207 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴))) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))) |
209 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴))) → (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) |
210 | 66 | ad2antll 729 |
. . . . . . . . . . . . . . . . . 18
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴))) → (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑢)
∩ (2nd ‘𝑣))))) |
211 | 208, 209,
210, 67 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) ∧ ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴))) → 𝑦 = 𝑤) |
212 | 211 | exp32 424 |
. . . . . . . . . . . . . . . 16
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤))) |
213 | 212 | impancom 455 |
. . . . . . . . . . . . . . 15
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) → ((𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤))) |
214 | 213 | expdimp 456 |
. . . . . . . . . . . . . 14
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (𝑣 ∈ (𝑆‘suc 𝑁) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤))) |
215 | 214 | rexlimdv 3210 |
. . . . . . . . . . . . 13
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)) |
216 | 90 | adantrd 495 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) → ((𝑥 =
∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤)) |
217 | 216 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤)) |
218 | 217 | ad3antlr 731 |
. . . . . . . . . . . . . 14
⊢ ((((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) ∧ 𝑖 ∈ ω) → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤)) |
219 | 218 | rexlimdva 3211 |
. . . . . . . . . . . . 13
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵) → 𝑦 = 𝑤)) |
220 | 215, 219 | jaod 859 |
. . . . . . . . . . . 12
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) ∧ 𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) → 𝑦 = 𝑤)) |
221 | 220 | rexlimdva 3211 |
. . . . . . . . . . 11
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) → 𝑦 = 𝑤)) |
222 | | simplll 775 |
. . . . . . . . . . . . . . . 16
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → Fun (𝑆‘suc 𝑁)) |
223 | 203 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁))) |
224 | 100 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (𝑢 ∈ (𝑆‘𝑁) → 𝑢 ∈ (𝑆‘suc 𝑁))) |
225 | 224 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (𝑢 ∈ (𝑆‘𝑁) → 𝑢 ∈ (𝑆‘suc 𝑁))) |
226 | 225 | com12 32 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 ∈ (𝑆‘𝑁) → (((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑢 ∈ (𝑆‘suc 𝑁))) |
227 | 226 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → (((Fun (𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑢 ∈ (𝑆‘suc 𝑁))) |
228 | 227 | impcom 411 |
. . . . . . . . . . . . . . . . 17
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑢 ∈ (𝑆‘suc 𝑁)) |
229 | 105 | ad2antll 729 |
. . . . . . . . . . . . . . . . 17
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → 𝑣 ∈ (𝑆‘suc 𝑁)) |
230 | 228, 229 | jca 515 |
. . . . . . . . . . . . . . . 16
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁))) |
231 | 222, 223,
230 | 3jca 1130 |
. . . . . . . . . . . . . . 15
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → (Fun (𝑆‘suc 𝑁) ∧ (𝑠 ∈ (𝑆‘suc 𝑁) ∧ 𝑟 ∈ (𝑆‘suc 𝑁)) ∧ (𝑢 ∈ (𝑆‘suc 𝑁) ∧ 𝑣 ∈ (𝑆‘suc 𝑁)))) |
232 | 231, 63, 66, 67 | syl3an 1162 |
. . . . . . . . . . . . . 14
⊢ (((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∧ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤) |
233 | 232 | 3exp 1121 |
. . . . . . . . . . . . 13
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤))) |
234 | 233 | impancom 455 |
. . . . . . . . . . . 12
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) → ((𝑢 ∈ (𝑆‘𝑁) ∧ 𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))) → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤))) |
235 | 234 | rexlimdvv 3220 |
. . . . . . . . . . 11
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) → (∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) → 𝑦 = 𝑤)) |
236 | 221, 235 | jaod 859 |
. . . . . . . . . 10
⊢ ((((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) ∧ (𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤)) |
237 | 236 | ex 416 |
. . . . . . . . 9
⊢ (((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) ∧ (𝑠 ∈ (𝑆‘𝑁) ∧ 𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁)))) → ((𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤))) |
238 | 237 | rexlimdvva 3221 |
. . . . . . . 8
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (∃𝑠 ∈ (𝑆‘𝑁)∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤))) |
239 | 195, 238 | jaod 859 |
. . . . . . 7
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → ((∃𝑠 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑟 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟)))) ∨ ∃𝑗 ∈ ω (𝑥 = ∀𝑔𝑗(1st ‘𝑠) ∧ 𝑦 = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑗, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑗}))) ∈ (2nd ‘𝑠)})) ∨ ∃𝑠 ∈ (𝑆‘𝑁)∃𝑟 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑠)⊼𝑔(1st
‘𝑟)) ∧ 𝑦 = ((𝑀 ↑m ω) ∖
((2nd ‘𝑠)
∩ (2nd ‘𝑟))))) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤))) |
240 | 53, 239 | syl5bi 245 |
. . . . . 6
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴)) → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)) → 𝑦 = 𝑤))) |
241 | 240 | impd 414 |
. . . . 5
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → (((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴)) ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴))) → 𝑦 = 𝑤)) |
242 | 241 | alrimivv 1936 |
. . . 4
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → ∀𝑦∀𝑤(((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴)) ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴))) → 𝑦 = 𝑤)) |
243 | | eqeq1 2742 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑤 → (𝑦 = 𝐴 ↔ 𝑤 = 𝐴)) |
244 | 243 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑦 = 𝑤 → ((𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ↔ (𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴))) |
245 | 244 | rexbidv 3224 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴))) |
246 | | eqeq1 2742 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑤 → (𝑦 = 𝐵 ↔ 𝑤 = 𝐵)) |
247 | 246 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑦 = 𝑤 → ((𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵) ↔ (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵))) |
248 | 247 | rexbidv 3224 |
. . . . . . . 8
⊢ (𝑦 = 𝑤 → (∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵) ↔ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵))) |
249 | 245, 248 | orbi12d 919 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → ((∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ↔ (∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)))) |
250 | 249 | rexbidv 3224 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ↔ ∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)))) |
251 | 244 | 2rexbidv 3227 |
. . . . . 6
⊢ (𝑦 = 𝑤 → (∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ↔ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴))) |
252 | 250, 251 | orbi12d 919 |
. . . . 5
⊢ (𝑦 = 𝑤 → ((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴)) ↔ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴)))) |
253 | 252 | mo4 2566 |
. . . 4
⊢
(∃*𝑦(∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴)) ↔ ∀𝑦∀𝑤(((∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴)) ∧ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑤 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑤 = 𝐴))) → 𝑦 = 𝑤)) |
254 | 242, 253 | sylibr 237 |
. . 3
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → ∃*𝑦(∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴))) |
255 | 254 | alrimiv 1935 |
. 2
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → ∀𝑥∃*𝑦(∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴))) |
256 | | funopab 6432 |
. 2
⊢ (Fun
{〈𝑥, 𝑦〉 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴))} ↔ ∀𝑥∃*𝑦(∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴))) |
257 | 255, 256 | sylibr 237 |
1
⊢ ((Fun
(𝑆‘suc 𝑁) ∧ (𝑆‘𝑁) ⊆ (𝑆‘suc 𝑁)) → Fun {〈𝑥, 𝑦〉 ∣ (∃𝑢 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(∃𝑣 ∈ (𝑆‘suc 𝑁)(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴) ∨ ∃𝑖 ∈ ω (𝑥 = ∀𝑔𝑖(1st ‘𝑢) ∧ 𝑦 = 𝐵)) ∨ ∃𝑢 ∈ (𝑆‘𝑁)∃𝑣 ∈ ((𝑆‘suc 𝑁) ∖ (𝑆‘𝑁))(𝑥 = ((1st ‘𝑢)⊼𝑔(1st
‘𝑣)) ∧ 𝑦 = 𝐴))}) |