Proof of Theorem bnj1446
| Step | Hyp | Ref
| Expression |
| 1 | | bnj1446.12 |
. . . . 5
⊢ 𝑄 = (𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) |
| 2 | | bnj1446.10 |
. . . . . . 7
⊢ 𝑃 = ∪
𝐻 |
| 3 | | bnj1446.9 |
. . . . . . . . 9
⊢ 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} |
| 4 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑
pred(𝑥, 𝐴, 𝑅) |
| 5 | | bnj1446.8 |
. . . . . . . . . . . 12
⊢ (𝜏′ ↔ [𝑦 / 𝑥]𝜏) |
| 6 | | nfcv 2905 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑑𝑦 |
| 7 | | bnj1446.4 |
. . . . . . . . . . . . . 14
⊢ (𝜏 ↔ (𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))) |
| 8 | | bnj1446.3 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
| 9 | | nfre1 3285 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑑∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌)) |
| 10 | 9 | nfab 2911 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑑{𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
| 11 | 8, 10 | nfcxfr 2903 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑑𝐶 |
| 12 | 11 | nfcri 2897 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑑 𝑓 ∈ 𝐶 |
| 13 | | nfv 1914 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑑dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)) |
| 14 | 12, 13 | nfan 1899 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑑(𝑓 ∈ 𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))) |
| 15 | 7, 14 | nfxfr 1853 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑑𝜏 |
| 16 | 6, 15 | nfsbcw 3810 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑑[𝑦 / 𝑥]𝜏 |
| 17 | 5, 16 | nfxfr 1853 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑𝜏′ |
| 18 | 4, 17 | nfrexw 3313 |
. . . . . . . . . 10
⊢
Ⅎ𝑑∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′ |
| 19 | 18 | nfab 2911 |
. . . . . . . . 9
⊢
Ⅎ𝑑{𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′} |
| 20 | 3, 19 | nfcxfr 2903 |
. . . . . . . 8
⊢
Ⅎ𝑑𝐻 |
| 21 | 20 | nfuni 4914 |
. . . . . . 7
⊢
Ⅎ𝑑∪ 𝐻 |
| 22 | 2, 21 | nfcxfr 2903 |
. . . . . 6
⊢
Ⅎ𝑑𝑃 |
| 23 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑑𝑥 |
| 24 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑑𝐺 |
| 25 | | bnj1446.11 |
. . . . . . . . . 10
⊢ 𝑍 = 〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
| 26 | 22, 4 | nfres 5999 |
. . . . . . . . . . 11
⊢
Ⅎ𝑑(𝑃 ↾ pred(𝑥, 𝐴, 𝑅)) |
| 27 | 23, 26 | nfop 4889 |
. . . . . . . . . 10
⊢
Ⅎ𝑑〈𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
| 28 | 25, 27 | nfcxfr 2903 |
. . . . . . . . 9
⊢
Ⅎ𝑑𝑍 |
| 29 | 24, 28 | nffv 6916 |
. . . . . . . 8
⊢
Ⅎ𝑑(𝐺‘𝑍) |
| 30 | 23, 29 | nfop 4889 |
. . . . . . 7
⊢
Ⅎ𝑑〈𝑥, (𝐺‘𝑍)〉 |
| 31 | 30 | nfsn 4707 |
. . . . . 6
⊢
Ⅎ𝑑{〈𝑥, (𝐺‘𝑍)〉} |
| 32 | 22, 31 | nfun 4170 |
. . . . 5
⊢
Ⅎ𝑑(𝑃 ∪ {〈𝑥, (𝐺‘𝑍)〉}) |
| 33 | 1, 32 | nfcxfr 2903 |
. . . 4
⊢
Ⅎ𝑑𝑄 |
| 34 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑑𝑧 |
| 35 | 33, 34 | nffv 6916 |
. . 3
⊢
Ⅎ𝑑(𝑄‘𝑧) |
| 36 | | bnj1446.13 |
. . . . 5
⊢ 𝑊 = 〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 |
| 37 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑑
pred(𝑧, 𝐴, 𝑅) |
| 38 | 33, 37 | nfres 5999 |
. . . . . 6
⊢
Ⅎ𝑑(𝑄 ↾ pred(𝑧, 𝐴, 𝑅)) |
| 39 | 34, 38 | nfop 4889 |
. . . . 5
⊢
Ⅎ𝑑〈𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))〉 |
| 40 | 36, 39 | nfcxfr 2903 |
. . . 4
⊢
Ⅎ𝑑𝑊 |
| 41 | 24, 40 | nffv 6916 |
. . 3
⊢
Ⅎ𝑑(𝐺‘𝑊) |
| 42 | 35, 41 | nfeq 2919 |
. 2
⊢
Ⅎ𝑑(𝑄‘𝑧) = (𝐺‘𝑊) |
| 43 | 42 | nf5ri 2195 |
1
⊢ ((𝑄‘𝑧) = (𝐺‘𝑊) → ∀𝑑(𝑄‘𝑧) = (𝐺‘𝑊)) |