Proof of Theorem bnj1446
Step | Hyp | Ref
| Expression |
1 | | bnj1446.12 |
. . . . 5
⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) |
2 | | bnj1446.10 |
. . . . . . 7
⊢ 𝑃 = ∪
𝐻 |
3 | | bnj1446.9 |
. . . . . . . . 9
⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} |
4 | | nfcv 2904 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑
pred(𝑥, 𝐴, 𝑅) |
5 | | bnj1446.8 |
. . . . . . . . . . . 12
⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) |
6 | | nfcv 2904 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑑𝑦 |
7 | | bnj1446.4 |
. . . . . . . . . . . . . 14
⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) |
8 | | bnj1446.3 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
9 | | nfre1 3225 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑑∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌)) |
10 | 9 | nfab 2910 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑑{𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
11 | 8, 10 | nfcxfr 2902 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑑𝐶 |
12 | 11 | nfcri 2891 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑑 𝑓 ∈ 𝐶 |
13 | | nfv 1922 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑑dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) |
14 | 12, 13 | nfan 1907 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑑(𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) |
15 | 7, 14 | nfxfr 1860 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑑𝜏 |
16 | 6, 15 | nfsbcw 3716 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑑[𝑦 / 𝑥]𝜏 |
17 | 5, 16 | nfxfr 1860 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑𝜏′ |
18 | 4, 17 | nfrex 3228 |
. . . . . . . . . 10
⊢
Ⅎ𝑑∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′ |
19 | 18 | nfab 2910 |
. . . . . . . . 9
⊢
Ⅎ𝑑{𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} |
20 | 3, 19 | nfcxfr 2902 |
. . . . . . . 8
⊢
Ⅎ𝑑𝐻 |
21 | 20 | nfuni 4826 |
. . . . . . 7
⊢
Ⅎ𝑑∪ 𝐻 |
22 | 2, 21 | nfcxfr 2902 |
. . . . . 6
⊢
Ⅎ𝑑𝑃 |
23 | | nfcv 2904 |
. . . . . . . 8
⊢
Ⅎ𝑑𝑥 |
24 | | nfcv 2904 |
. . . . . . . . 9
⊢
Ⅎ𝑑𝐺 |
25 | | bnj1446.11 |
. . . . . . . . . 10
⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
26 | 22, 4 | nfres 5853 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑(𝑃 ↾ pred(𝑥, 𝐴, 𝑅)) |
27 | 23, 26 | nfop 4800 |
. . . . . . . . . 10
⊢
Ⅎ𝑑〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
28 | 25, 27 | nfcxfr 2902 |
. . . . . . . . 9
⊢
Ⅎ𝑑𝑍 |
29 | 24, 28 | nffv 6727 |
. . . . . . . 8
⊢
Ⅎ𝑑(𝐺‘𝑍) |
30 | 23, 29 | nfop 4800 |
. . . . . . 7
⊢
Ⅎ𝑑〈𝑥, (𝐺‘𝑍)〉 |
31 | 30 | nfsn 4623 |
. . . . . 6
⊢
Ⅎ𝑑{〈𝑥, (𝐺‘𝑍)〉} |
32 | 22, 31 | nfun 4079 |
. . . . 5
⊢
Ⅎ𝑑(𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) |
33 | 1, 32 | nfcxfr 2902 |
. . . 4
⊢
Ⅎ𝑑𝑄 |
34 | | nfcv 2904 |
. . . 4
⊢
Ⅎ𝑑𝑧 |
35 | 33, 34 | nffv 6727 |
. . 3
⊢
Ⅎ𝑑(𝑄‘𝑧) |
36 | | bnj1446.13 |
. . . . 5
⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 |
37 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑑
pred(𝑧, 𝐴, 𝑅) |
38 | 33, 37 | nfres 5853 |
. . . . . 6
⊢
Ⅎ𝑑(𝑄 ↾ pred(𝑧, 𝐴, 𝑅)) |
39 | 34, 38 | nfop 4800 |
. . . . 5
⊢
Ⅎ𝑑〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 |
40 | 36, 39 | nfcxfr 2902 |
. . . 4
⊢
Ⅎ𝑑𝑊 |
41 | 24, 40 | nffv 6727 |
. . 3
⊢
Ⅎ𝑑(𝐺‘𝑊) |
42 | 35, 41 | nfeq 2917 |
. 2
⊢
Ⅎ𝑑(𝑄‘𝑧) = (𝐺‘𝑊) |
43 | 42 | nf5ri 2193 |
1
⊢ ((𝑄‘𝑧) = (𝐺‘𝑊) → ∀𝑑(𝑄‘𝑧) = (𝐺‘𝑊)) |