Proof of Theorem bnj1110
Step | Hyp | Ref
| Expression |
1 | | bnj1110.7 |
. . . . . . . . 9
⊢ 𝐷 = (ω ∖
{∅}) |
2 | 1 | bnj1098 32763 |
. . . . . . . 8
⊢
∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗)) |
3 | | bnj219 32712 |
. . . . . . . . . . 11
⊢ (𝑖 = suc 𝑗 → 𝑗 E 𝑖) |
4 | 3 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗) → 𝑗 E 𝑖) |
5 | 4 | ancli 549 |
. . . . . . . . 9
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗) → ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗) ∧ 𝑗 E 𝑖)) |
6 | | df-3an 1088 |
. . . . . . . . 9
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗) ∧ 𝑗 E 𝑖)) |
7 | 5, 6 | sylibr 233 |
. . . . . . . 8
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖)) |
8 | 2, 7 | bnj1023 32760 |
. . . . . . 7
⊢
∃𝑗((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖)) |
9 | | bnj1110.3 |
. . . . . . . . . . . 12
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
10 | 9 | bnj1232 32783 |
. . . . . . . . . . 11
⊢ (𝜒 → 𝑛 ∈ 𝐷) |
11 | 10 | 3ad2ant3 1134 |
. . . . . . . . . 10
⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒) → 𝑛 ∈ 𝐷) |
12 | | bnj1110.19 |
. . . . . . . . . . 11
⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) |
13 | 12 | bnj1232 32783 |
. . . . . . . . . 10
⊢ (𝜑0 → 𝑖 ∈ 𝑛) |
14 | 11, 13 | anim12ci 614 |
. . . . . . . . 9
⊢ (((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0) → (𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷)) |
15 | 14 | anim2i 617 |
. . . . . . . 8
⊢ ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷))) |
16 | | 3anass 1094 |
. . . . . . . 8
⊢ ((𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷) ↔ (𝑖 ≠ ∅ ∧ (𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷))) |
17 | 15, 16 | sylibr 233 |
. . . . . . 7
⊢ ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑖 ≠ ∅ ∧ 𝑖 ∈ 𝑛 ∧ 𝑛 ∈ 𝐷)) |
18 | 8, 17 | bnj1101 32764 |
. . . . . 6
⊢
∃𝑗((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖)) |
19 | | 3simpb 1148 |
. . . . . . . . 9
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) → (𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖)) |
20 | 12 | bnj1235 32784 |
. . . . . . . . . . 11
⊢ (𝜑0 → 𝜎) |
21 | 20 | ad2antll 726 |
. . . . . . . . . 10
⊢ ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → 𝜎) |
22 | | bnj1110.18 |
. . . . . . . . . 10
⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′)) |
23 | 21, 22 | sylib 217 |
. . . . . . . . 9
⊢ ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′)) |
24 | 19, 23 | syl5 34 |
. . . . . . . 8
⊢ ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) → 𝜂′)) |
25 | 24 | a2i 14 |
. . . . . . 7
⊢ (((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖)) → ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → 𝜂′)) |
26 | | pm3.43 474 |
. . . . . . 7
⊢ ((((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖)) ∧ ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → 𝜂′)) → ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′))) |
27 | 25, 26 | mpdan 684 |
. . . . . 6
⊢ (((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖)) → ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′))) |
28 | 18, 27 | bnj101 32702 |
. . . . 5
⊢
∃𝑗((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′)) |
29 | 12 | bnj1247 32788 |
. . . . . . 7
⊢ (𝜑0 → 𝑓 ∈ 𝐾) |
30 | 29 | ad2antll 726 |
. . . . . 6
⊢ ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → 𝑓 ∈ 𝐾) |
31 | | pm3.43i 473 |
. . . . . 6
⊢ (((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → 𝑓 ∈ 𝐾) → (((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′)) → ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑓 ∈ 𝐾 ∧ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′))))) |
32 | 30, 31 | ax-mp 5 |
. . . . 5
⊢ (((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′)) → ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑓 ∈ 𝐾 ∧ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′)))) |
33 | 28, 32 | bnj101 32702 |
. . . 4
⊢
∃𝑗((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑓 ∈ 𝐾 ∧ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′))) |
34 | | fndm 6536 |
. . . . . . . . 9
⊢ (𝑓 Fn 𝑛 → dom 𝑓 = 𝑛) |
35 | 9, 34 | bnj770 32743 |
. . . . . . . 8
⊢ (𝜒 → dom 𝑓 = 𝑛) |
36 | 35 | 3ad2ant3 1134 |
. . . . . . 7
⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒) → dom 𝑓 = 𝑛) |
37 | 36 | ad2antrl 725 |
. . . . . 6
⊢ ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → dom 𝑓 = 𝑛) |
38 | 37 | eleq2d 2824 |
. . . . 5
⊢ ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛)) |
39 | | pm3.43i 473 |
. . . . 5
⊢ (((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛)) → (((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑓 ∈ 𝐾 ∧ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′))) → ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑓 ∈ 𝐾 ∧ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′)))))) |
40 | 38, 39 | ax-mp 5 |
. . . 4
⊢ (((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑓 ∈ 𝐾 ∧ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′))) → ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑓 ∈ 𝐾 ∧ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′))))) |
41 | 33, 40 | bnj101 32702 |
. . 3
⊢
∃𝑗((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑓 ∈ 𝐾 ∧ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′)))) |
42 | | bnj268 32688 |
. . . . . 6
⊢ (((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ 𝑓 ∈ 𝐾 ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′) ↔ ((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′)) |
43 | | bnj251 32681 |
. . . . . 6
⊢ (((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ 𝑓 ∈ 𝐾 ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′) ↔ ((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑓 ∈ 𝐾 ∧ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′)))) |
44 | 42, 43 | bitr3i 276 |
. . . . 5
⊢ (((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′) ↔ ((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑓 ∈ 𝐾 ∧ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′)))) |
45 | 44 | imbi2i 336 |
. . . 4
⊢ (((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′)) ↔ ((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑓 ∈ 𝐾 ∧ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′))))) |
46 | 45 | exbii 1850 |
. . 3
⊢
(∃𝑗((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′)) ↔ ∃𝑗((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑓 ∈ 𝐾 ∧ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′))))) |
47 | 41, 46 | mpbir 230 |
. 2
⊢
∃𝑗((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → ((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′)) |
48 | | simp1 1135 |
. . . 4
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) → 𝑗 ∈ 𝑛) |
49 | 48 | bnj706 32734 |
. . 3
⊢ (((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′) → 𝑗 ∈ 𝑛) |
50 | | simp2 1136 |
. . . 4
⊢ ((𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) → 𝑖 = suc 𝑗) |
51 | 50 | bnj706 32734 |
. . 3
⊢ (((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′) → 𝑖 = suc 𝑗) |
52 | | bnj258 32687 |
. . . . 5
⊢ (((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′) ↔ (((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝜂′) ∧ 𝑓 ∈ 𝐾)) |
53 | 52 | simprbi 497 |
. . . 4
⊢ (((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′) → 𝑓 ∈ 𝐾) |
54 | | bnj642 32728 |
. . . . 5
⊢ (((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′) → (𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛)) |
55 | 49, 54 | mpbird 256 |
. . . 4
⊢ (((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′) → 𝑗 ∈ dom 𝑓) |
56 | | bnj645 32730 |
. . . . 5
⊢ (((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′) → 𝜂′) |
57 | | bnj1110.26 |
. . . . 5
⊢ (𝜂′ ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵)) |
58 | 56, 57 | sylib 217 |
. . . 4
⊢ (((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′) → ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵)) |
59 | 53, 55, 58 | mp2and 696 |
. . 3
⊢ (((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′) → (𝑓‘𝑗) ⊆ 𝐵) |
60 | 49, 51, 59 | 3jca 1127 |
. 2
⊢ (((𝑗 ∈ dom 𝑓 ↔ 𝑗 ∈ 𝑛) ∧ (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ 𝑗 E 𝑖) ∧ 𝑓 ∈ 𝐾 ∧ 𝜂′) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ (𝑓‘𝑗) ⊆ 𝐵)) |
61 | 47, 60 | bnj1023 32760 |
1
⊢
∃𝑗((𝑖 ≠ ∅ ∧ ((𝜃 ∧ 𝜏 ∧ 𝜒) ∧ 𝜑0)) → (𝑗 ∈ 𝑛 ∧ 𝑖 = suc 𝑗 ∧ (𝑓‘𝑗) ⊆ 𝐵)) |