Step | Hyp | Ref
| Expression |
1 | | bnj600.5 |
. . . . . 6
⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒)) |
2 | | bnj600.13 |
. . . . . 6
⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑) |
3 | | bnj600.14 |
. . . . . 6
⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓) |
4 | | bnj600.17 |
. . . . . 6
⊢ (𝜏 ↔ (𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′)) |
5 | | bnj600.19 |
. . . . . 6
⊢ (𝜂 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) |
6 | | bnj600.16 |
. . . . . . 7
⊢ 𝐺 = (𝑓 ∪ {〈𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)〉}) |
7 | 6 | bnj528 32443 |
. . . . . 6
⊢ 𝐺 ∈ V |
8 | | bnj600.4 |
. . . . . . 7
⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
9 | | bnj600.10 |
. . . . . . 7
⊢ (𝜑′ ↔ [𝑚 / 𝑛]𝜑) |
10 | | bnj600.11 |
. . . . . . 7
⊢ (𝜓′ ↔ [𝑚 / 𝑛]𝜓) |
11 | | bnj600.12 |
. . . . . . 7
⊢ (𝜒′ ↔ [𝑚 / 𝑛]𝜒) |
12 | | vex 3403 |
. . . . . . 7
⊢ 𝑚 ∈ V |
13 | 8, 9, 10, 11, 12 | bnj207 32435 |
. . . . . 6
⊢ (𝜒′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑚 ∧ 𝜑′ ∧ 𝜓′))) |
14 | | bnj600.1 |
. . . . . . 7
⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
15 | 14, 2, 7 | bnj609 32471 |
. . . . . 6
⊢ (𝜑″ ↔ (𝐺‘∅) = pred(𝑥, 𝐴, 𝑅)) |
16 | | bnj600.2 |
. . . . . . 7
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
17 | 16, 3, 7 | bnj611 32472 |
. . . . . 6
⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
18 | | bnj600.3 |
. . . . . . . . . 10
⊢ 𝐷 = (ω ∖
{∅}) |
19 | 18 | bnj168 32282 |
. . . . . . . . 9
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚 ∈ 𝐷 𝑛 = suc 𝑚) |
20 | | df-rex 3060 |
. . . . . . . . 9
⊢
(∃𝑚 ∈
𝐷 𝑛 = suc 𝑚 ↔ ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚)) |
21 | 19, 20 | sylib 221 |
. . . . . . . 8
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚)) |
22 | 18 | bnj158 32281 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ 𝐷 → ∃𝑝 ∈ ω 𝑚 = suc 𝑝) |
23 | | df-rex 3060 |
. . . . . . . . . . . . . 14
⊢
(∃𝑝 ∈
ω 𝑚 = suc 𝑝 ↔ ∃𝑝(𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) |
24 | 22, 23 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ 𝐷 → ∃𝑝(𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) |
25 | 24 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚) → ∃𝑝(𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) |
26 | 25 | ancri 553 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚) → (∃𝑝(𝑝 ∈ ω ∧ 𝑚 = suc 𝑝) ∧ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚))) |
27 | 26 | bnj534 32292 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚) → ∃𝑝((𝑝 ∈ ω ∧ 𝑚 = suc 𝑝) ∧ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚))) |
28 | | bnj432 32268 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝) ↔ ((𝑝 ∈ ω ∧ 𝑚 = suc 𝑝) ∧ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚))) |
29 | 28 | exbii 1854 |
. . . . . . . . . 10
⊢
(∃𝑝(𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝) ↔ ∃𝑝((𝑝 ∈ ω ∧ 𝑚 = suc 𝑝) ∧ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚))) |
30 | 27, 29 | sylibr 237 |
. . . . . . . . 9
⊢ ((𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚) → ∃𝑝(𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) |
31 | 30 | eximi 1841 |
. . . . . . . 8
⊢
(∃𝑚(𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚) → ∃𝑚∃𝑝(𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) |
32 | 21, 31 | syl 17 |
. . . . . . 7
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚∃𝑝(𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) |
33 | 5 | 2exbii 1855 |
. . . . . . 7
⊢
(∃𝑚∃𝑝𝜂 ↔ ∃𝑚∃𝑝(𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝)) |
34 | 32, 33 | sylibr 237 |
. . . . . 6
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷) → ∃𝑚∃𝑝𝜂) |
35 | | rsp 3119 |
. . . . . . . . 9
⊢
(∀𝑚 ∈
𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒) → (𝑚 ∈ 𝐷 → (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒))) |
36 | 1, 35 | sylbi 220 |
. . . . . . . 8
⊢ (𝜃 → (𝑚 ∈ 𝐷 → (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒))) |
37 | 36 | 3imp 1112 |
. . . . . . 7
⊢ ((𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛) → [𝑚 / 𝑛]𝜒) |
38 | 37, 11 | sylibr 237 |
. . . . . 6
⊢ ((𝜃 ∧ 𝑚 ∈ 𝐷 ∧ 𝑚 E 𝑛) → 𝜒′) |
39 | | bnj600.18 |
. . . . . . 7
⊢ (𝜎 ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚)) |
40 | 14, 9, 12 | bnj523 32441 |
. . . . . . . 8
⊢ (𝜑′ ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅)) |
41 | 16, 10, 12 | bnj539 32445 |
. . . . . . . 8
⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑚 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
42 | 40, 41, 18, 6, 4, 39 | bnj544 32448 |
. . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝐺 Fn 𝑛) |
43 | 39, 5, 42 | bnj561 32457 |
. . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝐺 Fn 𝑛) |
44 | 40, 18, 6, 4, 39, 42, 15 | bnj545 32449 |
. . . . . . 7
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜎) → 𝜑″) |
45 | 39, 5, 44 | bnj562 32458 |
. . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜑″) |
46 | | bnj600.20 |
. . . . . . 7
⊢ (𝜁 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖)) |
47 | | bnj600.22 |
. . . . . . 7
⊢ 𝐵 = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) |
48 | | bnj600.23 |
. . . . . . 7
⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) |
49 | | bnj600.24 |
. . . . . . 7
⊢ 𝐾 = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅) |
50 | | bnj600.25 |
. . . . . . 7
⊢ 𝐿 = ∪ 𝑦 ∈ (𝐺‘𝑝) pred(𝑦, 𝐴, 𝑅) |
51 | | bnj600.26 |
. . . . . . 7
⊢ 𝐺 = (𝑓 ∪ {〈𝑚, 𝐶〉}) |
52 | | bnj600.21 |
. . . . . . 7
⊢ (𝜌 ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖)) |
53 | 18, 6, 4, 39, 5, 46, 47, 48, 49, 50, 51, 40, 41, 42, 52, 43, 17 | bnj571 32460 |
. . . . . 6
⊢ ((𝑅 FrSe 𝐴 ∧ 𝜏 ∧ 𝜂) → 𝜓″) |
54 | | biid 264 |
. . . . . 6
⊢
([𝑧 / 𝑓]𝜑 ↔ [𝑧 / 𝑓]𝜑) |
55 | | biid 264 |
. . . . . 6
⊢
([𝑧 / 𝑓]𝜓 ↔ [𝑧 / 𝑓]𝜓) |
56 | | biid 264 |
. . . . . 6
⊢
([𝐺 / 𝑧][𝑧 / 𝑓]𝜑 ↔ [𝐺 / 𝑧][𝑧 / 𝑓]𝜑) |
57 | | biid 264 |
. . . . . 6
⊢
([𝐺 / 𝑧][𝑧 / 𝑓]𝜓 ↔ [𝐺 / 𝑧][𝑧 / 𝑓]𝜓) |
58 | 1, 2, 3, 4, 5, 7, 13, 15, 17, 34, 38, 43, 45, 53, 14, 16, 54, 55, 56, 57 | bnj607 32470 |
. . . . 5
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃) → ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
59 | 14, 16, 18 | bnj579 32468 |
. . . . . . 7
⊢ (𝑛 ∈ 𝐷 → ∃*𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
60 | 59 | a1d 25 |
. . . . . 6
⊢ (𝑛 ∈ 𝐷 → ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
61 | 60 | 3ad2ant2 1135 |
. . . . 5
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃) → ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃*𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
62 | 58, 61 | jcad 516 |
. . . 4
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃) → ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (∃𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) ∧ ∃*𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))) |
63 | | df-eu 2571 |
. . . 4
⊢
(∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) ↔ (∃𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) ∧ ∃*𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
64 | 62, 63 | syl6ibr 255 |
. . 3
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃) → ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))) |
65 | 64, 8 | sylibr 237 |
. 2
⊢ ((𝑛 ≠ 1o ∧ 𝑛 ∈ 𝐷 ∧ 𝜃) → 𝜒) |
66 | 65 | 3expib 1123 |
1
⊢ (𝑛 ≠ 1o →
((𝑛 ∈ 𝐷 ∧ 𝜃) → 𝜒)) |