Step | Hyp | Ref
| Expression |
1 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑛if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)) |
2 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑚if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛)) |
3 | | fveq2 6103 |
. . . . 5
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
4 | 3 | eqeq1d 2612 |
. . . 4
⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) = ∅ ↔ (𝐹‘𝑛) = ∅)) |
5 | 4, 3 | ifbieq2d 4061 |
. . 3
⊢ (𝑚 = 𝑛 → if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)) = if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛))) |
6 | 1, 2, 5 | cbvmpt 4677 |
. 2
⊢ (𝑚 ∈ ω ↦
if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚))) = (𝑛 ∈ ω ↦ if((𝐹‘𝑛) = ∅, {∅}, (𝐹‘𝑛))) |
7 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑛({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚)) |
8 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑚{𝑛} |
9 | | nffvmpt1 6111 |
. . . 4
⊢
Ⅎ𝑚((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑛) |
10 | 8, 9 | nfxp 5066 |
. . 3
⊢
Ⅎ𝑚({𝑛} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑛)) |
11 | | sneq 4135 |
. . . 4
⊢ (𝑚 = 𝑛 → {𝑚} = {𝑛}) |
12 | | fveq2 6103 |
. . . 4
⊢ (𝑚 = 𝑛 → ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚) = ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑛)) |
13 | 11, 12 | xpeq12d 5064 |
. . 3
⊢ (𝑚 = 𝑛 → ({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚)) = ({𝑛} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑛))) |
14 | 7, 10, 13 | cbvmpt 4677 |
. 2
⊢ (𝑚 ∈ ω ↦ ({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚))) = (𝑛 ∈ ω ↦ ({𝑛} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑛))) |
15 | | nfcv 2751 |
. . 3
⊢
Ⅎ𝑛(2nd ‘(𝑓‘((𝑚 ∈ ω ↦ ({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚)))‘𝑚))) |
16 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑚2nd |
17 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑚𝑓 |
18 | | nffvmpt1 6111 |
. . . . 5
⊢
Ⅎ𝑚((𝑚 ∈ ω ↦ ({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚)))‘𝑛) |
19 | 17, 18 | nffv 6110 |
. . . 4
⊢
Ⅎ𝑚(𝑓‘((𝑚 ∈ ω ↦ ({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚)))‘𝑛)) |
20 | 16, 19 | nffv 6110 |
. . 3
⊢
Ⅎ𝑚(2nd ‘(𝑓‘((𝑚 ∈ ω ↦ ({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚)))‘𝑛))) |
21 | | fveq2 6103 |
. . . . 5
⊢ (𝑚 = 𝑛 → ((𝑚 ∈ ω ↦ ({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚)))‘𝑚) = ((𝑚 ∈ ω ↦ ({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚)))‘𝑛)) |
22 | 21 | fveq2d 6107 |
. . . 4
⊢ (𝑚 = 𝑛 → (𝑓‘((𝑚 ∈ ω ↦ ({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚)))‘𝑚)) = (𝑓‘((𝑚 ∈ ω ↦ ({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚)))‘𝑛))) |
23 | 22 | fveq2d 6107 |
. . 3
⊢ (𝑚 = 𝑛 → (2nd ‘(𝑓‘((𝑚 ∈ ω ↦ ({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚)))‘𝑚))) = (2nd ‘(𝑓‘((𝑚 ∈ ω ↦ ({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚)))‘𝑛)))) |
24 | 15, 20, 23 | cbvmpt 4677 |
. 2
⊢ (𝑚 ∈ ω ↦
(2nd ‘(𝑓‘((𝑚 ∈ ω ↦ ({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚)))‘𝑚)))) = (𝑛 ∈ ω ↦ (2nd
‘(𝑓‘((𝑚 ∈ ω ↦ ({𝑚} × ((𝑚 ∈ ω ↦ if((𝐹‘𝑚) = ∅, {∅}, (𝐹‘𝑚)))‘𝑚)))‘𝑛)))) |
25 | 6, 14, 24 | axcc2lem 9141 |
1
⊢
∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω ((𝐹‘𝑛) ≠ ∅ → (𝑔‘𝑛) ∈ (𝐹‘𝑛))) |