Step | Hyp | Ref
| Expression |
1 | | bnj865.1 |
. . . . . . 7
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑋, 𝐴, 𝑅)) |
2 | | bnj865.2 |
. . . . . . 7
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
3 | | bnj865.3 |
. . . . . . 7
⊢ 𝐷 = (ω ∖
{∅}) |
4 | 1, 2, 3 | bnj852 32614 |
. . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑛 ∈ 𝐷 ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
5 | | omex 9258 |
. . . . . . . . 9
⊢ ω
∈ V |
6 | | difexg 5220 |
. . . . . . . . 9
⊢ (ω
∈ V → (ω ∖ {∅}) ∈ V) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . 8
⊢ (ω
∖ {∅}) ∈ V |
8 | 3, 7 | eqeltri 2834 |
. . . . . . 7
⊢ 𝐷 ∈ V |
9 | | raleq 3319 |
. . . . . . . 8
⊢ (𝑧 = 𝐷 → (∀𝑛 ∈ 𝑧 ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) ↔ ∀𝑛 ∈ 𝐷 ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
10 | | raleq 3319 |
. . . . . . . . 9
⊢ (𝑧 = 𝐷 → (∀𝑛 ∈ 𝑧 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) ↔ ∀𝑛 ∈ 𝐷 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
11 | 10 | exbidv 1929 |
. . . . . . . 8
⊢ (𝑧 = 𝐷 → (∃𝑤∀𝑛 ∈ 𝑧 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) ↔ ∃𝑤∀𝑛 ∈ 𝐷 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
12 | 9, 11 | imbi12d 348 |
. . . . . . 7
⊢ (𝑧 = 𝐷 → ((∀𝑛 ∈ 𝑧 ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → ∃𝑤∀𝑛 ∈ 𝑧 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ (∀𝑛 ∈ 𝐷 ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → ∃𝑤∀𝑛 ∈ 𝐷 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))) |
13 | | zfrep6 7728 |
. . . . . . 7
⊢
(∀𝑛 ∈
𝑧 ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → ∃𝑤∀𝑛 ∈ 𝑧 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
14 | 8, 12, 13 | vtocl 3474 |
. . . . . 6
⊢
(∀𝑛 ∈
𝐷 ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) → ∃𝑤∀𝑛 ∈ 𝐷 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
15 | 4, 14 | syl 17 |
. . . . 5
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃𝑤∀𝑛 ∈ 𝐷 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
16 | | 19.37v 2000 |
. . . . 5
⊢
(∃𝑤((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑛 ∈ 𝐷 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃𝑤∀𝑛 ∈ 𝐷 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
17 | 15, 16 | mpbir 234 |
. . . 4
⊢
∃𝑤((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑛 ∈ 𝐷 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
18 | | df-ral 3066 |
. . . . . . . 8
⊢
(∀𝑛 ∈
𝐷 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) ↔ ∀𝑛(𝑛 ∈ 𝐷 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
19 | 18 | imbi2i 339 |
. . . . . . 7
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑛 ∈ 𝐷 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑛(𝑛 ∈ 𝐷 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))) |
20 | | 19.21v 1947 |
. . . . . . 7
⊢
(∀𝑛((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑛 ∈ 𝐷 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑛(𝑛 ∈ 𝐷 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))) |
21 | 19, 20 | bitr4i 281 |
. . . . . 6
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑛 ∈ 𝐷 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ∀𝑛((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑛 ∈ 𝐷 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))) |
22 | 21 | exbii 1855 |
. . . . 5
⊢
(∃𝑤((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑛 ∈ 𝐷 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ∃𝑤∀𝑛((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑛 ∈ 𝐷 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))) |
23 | | impexp 454 |
. . . . . . . 8
⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑛 ∈ 𝐷) → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑛 ∈ 𝐷 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))) |
24 | | df-3an 1091 |
. . . . . . . . . 10
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑛 ∈ 𝐷)) |
25 | 24 | bicomi 227 |
. . . . . . . . 9
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑛 ∈ 𝐷) ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷)) |
26 | 25 | imbi1i 353 |
. . . . . . . 8
⊢ ((((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑛 ∈ 𝐷) → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
27 | 23, 26 | bitr3i 280 |
. . . . . . 7
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑛 ∈ 𝐷 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
28 | 27 | albii 1827 |
. . . . . 6
⊢
(∀𝑛((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑛 ∈ 𝐷 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) ↔ ∀𝑛((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
29 | 28 | exbii 1855 |
. . . . 5
⊢
(∃𝑤∀𝑛((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑛 ∈ 𝐷 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) ↔ ∃𝑤∀𝑛((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
30 | 22, 29 | bitri 278 |
. . . 4
⊢
(∃𝑤((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴) → ∀𝑛 ∈ 𝐷 ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ∃𝑤∀𝑛((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
31 | 17, 30 | mpbi 233 |
. . 3
⊢
∃𝑤∀𝑛((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
32 | | bnj865.5 |
. . . . . . 7
⊢ (𝜒 ↔ (𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷)) |
33 | 32 | bicomi 227 |
. . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) ↔ 𝜒) |
34 | 33 | imbi1i 353 |
. . . . 5
⊢ (((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ (𝜒 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
35 | 34 | albii 1827 |
. . . 4
⊢
(∀𝑛((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
36 | 35 | exbii 1855 |
. . 3
⊢
(∃𝑤∀𝑛((𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷) → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
37 | 31, 36 | mpbi 233 |
. 2
⊢
∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
38 | | bnj865.6 |
. . . . . 6
⊢ (𝜃 ↔ (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
39 | 38 | rexbii 3170 |
. . . . 5
⊢
(∃𝑓 ∈
𝑤 𝜃 ↔ ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
40 | 39 | imbi2i 339 |
. . . 4
⊢ ((𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ↔ (𝜒 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
41 | 40 | albii 1827 |
. . 3
⊢
(∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ↔ ∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
42 | 41 | exbii 1855 |
. 2
⊢
(∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) ↔ ∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
43 | 37, 42 | mpbir 234 |
1
⊢
∃𝑤∀𝑛(𝜒 → ∃𝑓 ∈ 𝑤 𝜃) |