Proof of Theorem bnj1445
Step | Hyp | Ref
| Expression |
1 | | bnj1445.21 |
. 2
⊢ (𝜎 ↔ (𝜌 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)))) |
2 | | bnj1445.20 |
. . . . 5
⊢ (𝜌 ↔ (𝜁 ∧ 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓)) |
3 | | bnj1445.19 |
. . . . . . 7
⊢ (𝜁 ↔ (𝜃 ∧ 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅))) |
4 | | bnj1445.17 |
. . . . . . . . 9
⊢ (𝜃 ↔ (𝜒 ∧ 𝑧 ∈ 𝐸)) |
5 | | bnj1445.7 |
. . . . . . . . . . . . 13
⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥)) |
6 | | bnj1445.6 |
. . . . . . . . . . . . . . 15
⊢ (𝜓 ↔ (𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅)) |
7 | | nfv 1920 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑑 𝑅 FrSe 𝐴 |
8 | | bnj1445.5 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} |
9 | | bnj1445.4 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) |
10 | | bnj1445.3 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
11 | | nfre1 3236 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
Ⅎ𝑑∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌)) |
12 | 11 | nfab 2914 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑑{𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
13 | 10, 12 | nfcxfr 2906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑑𝐶 |
14 | 13 | nfcri 2895 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑑 𝑓 ∈ 𝐶 |
15 | | nfv 1920 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑑dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) |
16 | 14, 15 | nfan 1905 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑑(𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) |
17 | 9, 16 | nfxfr 1858 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑑𝜏 |
18 | 17 | nfex 2321 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑑∃𝑓𝜏 |
19 | 18 | nfn 1863 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑑 ¬
∃𝑓𝜏 |
20 | | nfcv 2908 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑑𝐴 |
21 | 19, 20 | nfrabw 3316 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑑{𝑥 ∈ 𝐴 ∣ ¬ ∃𝑓𝜏} |
22 | 8, 21 | nfcxfr 2906 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑑𝐷 |
23 | | nfcv 2908 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑑∅ |
24 | 22, 23 | nfne 3046 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑑 𝐷 ≠ ∅ |
25 | 7, 24 | nfan 1905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑑(𝑅 FrSe 𝐴 ∧ 𝐷 ≠ ∅) |
26 | 6, 25 | nfxfr 1858 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑑𝜓 |
27 | 22 | nfcri 2895 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑑 𝑥 ∈ 𝐷 |
28 | | nfv 1920 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑑 ¬ 𝑦𝑅𝑥 |
29 | 22, 28 | nfralw 3151 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑑∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥 |
30 | 26, 27, 29 | nf3an 1907 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑑(𝜓 ∧ 𝑥 ∈ 𝐷 ∧ ∀𝑦 ∈ 𝐷 ¬ 𝑦𝑅𝑥) |
31 | 5, 30 | nfxfr 1858 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑑𝜒 |
32 | 31 | nf5ri 2191 |
. . . . . . . . . . 11
⊢ (𝜒 → ∀𝑑𝜒) |
33 | 32 | bnj1351 32785 |
. . . . . . . . . 10
⊢ ((𝜒 ∧ 𝑧 ∈ 𝐸) → ∀𝑑(𝜒 ∧ 𝑧 ∈ 𝐸)) |
34 | 33 | nf5i 2145 |
. . . . . . . . 9
⊢
Ⅎ𝑑(𝜒 ∧ 𝑧 ∈ 𝐸) |
35 | 4, 34 | nfxfr 1858 |
. . . . . . . 8
⊢
Ⅎ𝑑𝜃 |
36 | | nfv 1920 |
. . . . . . . 8
⊢
Ⅎ𝑑 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅) |
37 | 35, 36 | nfan 1905 |
. . . . . . 7
⊢
Ⅎ𝑑(𝜃 ∧ 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅)) |
38 | 3, 37 | nfxfr 1858 |
. . . . . 6
⊢
Ⅎ𝑑𝜁 |
39 | | bnj1445.9 |
. . . . . . . 8
⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} |
40 | | nfcv 2908 |
. . . . . . . . . 10
⊢
Ⅎ𝑑
pred(𝑥, 𝐴, 𝑅) |
41 | | bnj1445.8 |
. . . . . . . . . . 11
⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) |
42 | | nfcv 2908 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑑𝑦 |
43 | 42, 17 | nfsbcw 3741 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑[𝑦 / 𝑥]𝜏 |
44 | 41, 43 | nfxfr 1858 |
. . . . . . . . . 10
⊢
Ⅎ𝑑𝜏′ |
45 | 40, 44 | nfrex 3239 |
. . . . . . . . 9
⊢
Ⅎ𝑑∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′ |
46 | 45 | nfab 2914 |
. . . . . . . 8
⊢
Ⅎ𝑑{𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} |
47 | 39, 46 | nfcxfr 2906 |
. . . . . . 7
⊢
Ⅎ𝑑𝐻 |
48 | 47 | nfcri 2895 |
. . . . . 6
⊢
Ⅎ𝑑 𝑓 ∈ 𝐻 |
49 | | nfv 1920 |
. . . . . 6
⊢
Ⅎ𝑑 𝑧 ∈ dom 𝑓 |
50 | 38, 48, 49 | nf3an 1907 |
. . . . 5
⊢
Ⅎ𝑑(𝜁 ∧ 𝑓 ∈ 𝐻 ∧ 𝑧 ∈ dom 𝑓) |
51 | 2, 50 | nfxfr 1858 |
. . . 4
⊢
Ⅎ𝑑𝜌 |
52 | 51 | nf5ri 2191 |
. . 3
⊢ (𝜌 → ∀𝑑𝜌) |
53 | | ax-5 1916 |
. . 3
⊢ (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → ∀𝑑 𝑦 ∈ pred(𝑥, 𝐴, 𝑅)) |
54 | 14 | nf5ri 2191 |
. . 3
⊢ (𝑓 ∈ 𝐶 → ∀𝑑 𝑓 ∈ 𝐶) |
55 | | ax-5 1916 |
. . 3
⊢ (dom
𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)) → ∀𝑑dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))) |
56 | 52, 53, 54, 55 | bnj982 32737 |
. 2
⊢ ((𝜌 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))) → ∀𝑑(𝜌 ∧ 𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)))) |
57 | 1, 56 | hbxfrbi 1830 |
1
⊢ (𝜎 → ∀𝑑𝜎) |