Proof of Theorem bnj1090
Step | Hyp | Ref
| Expression |
1 | | bnj1090.28 |
. 2
⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵)) |
2 | | impexp 454 |
. . . . . . 7
⊢ (((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂) ↔ (𝑖 ∈ 𝑛 → (𝜎 → 𝜂))) |
3 | 2 | exbii 1855 |
. . . . . 6
⊢
(∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂) ↔ ∃𝑗(𝑖 ∈ 𝑛 → (𝜎 → 𝜂))) |
4 | | bnj1090.18 |
. . . . . . . . . 10
⊢ (𝜎 ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′)) |
5 | 4 | imbi1i 353 |
. . . . . . . . 9
⊢ ((𝜎 → 𝜂) ↔ (((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂)) |
6 | 5 | exbii 1855 |
. . . . . . . 8
⊢
(∃𝑗(𝜎 → 𝜂) ↔ ∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂)) |
7 | 6 | imbi2i 339 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝑛 → ∃𝑗(𝜎 → 𝜂)) ↔ (𝑖 ∈ 𝑛 → ∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))) |
8 | | 19.37v 2000 |
. . . . . . 7
⊢
(∃𝑗(𝑖 ∈ 𝑛 → (𝜎 → 𝜂)) ↔ (𝑖 ∈ 𝑛 → ∃𝑗(𝜎 → 𝜂))) |
9 | | bnj1090.10 |
. . . . . . . . . . . 12
⊢ (𝜌 ↔ ∀𝑗 ∈ 𝑛 (𝑗 E 𝑖 → [𝑗 / 𝑖]𝜂)) |
10 | 9 | bnj115 32416 |
. . . . . . . . . . 11
⊢ (𝜌 ↔ ∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂)) |
11 | | bnj1090.17 |
. . . . . . . . . . . . 13
⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂) |
12 | 11 | imbi2i 339 |
. . . . . . . . . . . 12
⊢ (((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) ↔ ((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂)) |
13 | 12 | albii 1827 |
. . . . . . . . . . 11
⊢
(∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) ↔ ∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → [𝑗 / 𝑖]𝜂)) |
14 | 10, 13 | bitr4i 281 |
. . . . . . . . . 10
⊢ (𝜌 ↔ ∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′)) |
15 | 14 | imbi1i 353 |
. . . . . . . . 9
⊢ ((𝜌 → 𝜂) ↔ (∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂)) |
16 | | 19.36v 1996 |
. . . . . . . . 9
⊢
(∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂) ↔ (∀𝑗((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂)) |
17 | 15, 16 | bitr4i 281 |
. . . . . . . 8
⊢ ((𝜌 → 𝜂) ↔ ∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂)) |
18 | 17 | imbi2i 339 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝑛 → (𝜌 → 𝜂)) ↔ (𝑖 ∈ 𝑛 → ∃𝑗(((𝑗 ∈ 𝑛 ∧ 𝑗 E 𝑖) → 𝜂′) → 𝜂))) |
19 | 7, 8, 18 | 3bitr4i 306 |
. . . . . 6
⊢
(∃𝑗(𝑖 ∈ 𝑛 → (𝜎 → 𝜂)) ↔ (𝑖 ∈ 𝑛 → (𝜌 → 𝜂))) |
20 | 3, 19 | bitr2i 279 |
. . . . 5
⊢ ((𝑖 ∈ 𝑛 → (𝜌 → 𝜂)) ↔ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂)) |
21 | | impexp 454 |
. . . . . 6
⊢ ((((𝑖 ∈ 𝑛 ∧ 𝜎) ∧ (𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎) → ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))) |
22 | | bnj256 32397 |
. . . . . . 7
⊢ ((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎) ∧ (𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓))) |
23 | 22 | imbi1i 353 |
. . . . . 6
⊢ (((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵) ↔ (((𝑖 ∈ 𝑛 ∧ 𝜎) ∧ (𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) → (𝑓‘𝑖) ⊆ 𝐵)) |
24 | | bnj1090.9 |
. . . . . . 7
⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) |
25 | 24 | imbi2i 339 |
. . . . . 6
⊢ (((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎) → ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵))) |
26 | 21, 23, 25 | 3bitr4i 306 |
. . . . 5
⊢ (((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎) → 𝜂)) |
27 | 20, 26 | bnj133 32418 |
. . . 4
⊢ ((𝑖 ∈ 𝑛 → (𝜌 → 𝜂)) ↔ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) |
28 | 27 | albii 1827 |
. . 3
⊢
(∀𝑖(𝑖 ∈ 𝑛 → (𝜌 → 𝜂)) ↔ ∀𝑖∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) |
29 | | df-ral 3066 |
. . 3
⊢
(∀𝑖 ∈
𝑛 (𝜌 → 𝜂) ↔ ∀𝑖(𝑖 ∈ 𝑛 → (𝜌 → 𝜂))) |
30 | | bnj1090.19 |
. . . . . 6
⊢ (𝜑0 ↔ (𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓)) |
31 | 30 | imbi1i 353 |
. . . . 5
⊢ ((𝜑0 → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) |
32 | 31 | exbii 1855 |
. . . 4
⊢
(∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵) ↔ ∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) |
33 | 32 | albii 1827 |
. . 3
⊢
(∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵) ↔ ∀𝑖∃𝑗((𝑖 ∈ 𝑛 ∧ 𝜎 ∧ 𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) |
34 | 28, 29, 33 | 3bitr4i 306 |
. 2
⊢
(∀𝑖 ∈
𝑛 (𝜌 → 𝜂) ↔ ∀𝑖∃𝑗(𝜑0 → (𝑓‘𝑖) ⊆ 𝐵)) |
35 | 1, 34 | sylibr 237 |
1
⊢ ((𝜃 ∧ 𝜏 ∧ 𝜒 ∧ 𝜁) → ∀𝑖 ∈ 𝑛 (𝜌 → 𝜂)) |