Proof of Theorem bnj66
Step | Hyp | Ref
| Expression |
1 | | bnj66.3 |
. . . 4
⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
2 | | fneq1 6470 |
. . . . . . 7
⊢ (𝑔 = 𝑓 → (𝑔 Fn 𝑑 ↔ 𝑓 Fn 𝑑)) |
3 | | fveq1 6716 |
. . . . . . . . 9
⊢ (𝑔 = 𝑓 → (𝑔‘𝑥) = (𝑓‘𝑥)) |
4 | | reseq1 5845 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑓 → (𝑔 ↾ pred(𝑥, 𝐴, 𝑅)) = (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))) |
5 | 4 | opeq2d 4791 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑓 → 〈𝑥, (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))〉 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉) |
6 | | bnj66.2 |
. . . . . . . . . . 11
⊢ 𝑌 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
7 | 5, 6 | eqtr4di 2796 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑓 → 〈𝑥, (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))〉 = 𝑌) |
8 | 7 | fveq2d 6721 |
. . . . . . . . 9
⊢ (𝑔 = 𝑓 → (𝐺‘〈𝑥, (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))〉) = (𝐺‘𝑌)) |
9 | 3, 8 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑔 = 𝑓 → ((𝑔‘𝑥) = (𝐺‘〈𝑥, (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))〉) ↔ (𝑓‘𝑥) = (𝐺‘𝑌))) |
10 | 9 | ralbidv 3118 |
. . . . . . 7
⊢ (𝑔 = 𝑓 → (∀𝑥 ∈ 𝑑 (𝑔‘𝑥) = (𝐺‘〈𝑥, (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))〉) ↔ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))) |
11 | 2, 10 | anbi12d 634 |
. . . . . 6
⊢ (𝑔 = 𝑓 → ((𝑔 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑔‘𝑥) = (𝐺‘〈𝑥, (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))〉)) ↔ (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌)))) |
12 | 11 | rexbidv 3216 |
. . . . 5
⊢ (𝑔 = 𝑓 → (∃𝑑 ∈ 𝐵 (𝑔 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑔‘𝑥) = (𝐺‘〈𝑥, (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))〉)) ↔ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌)))) |
13 | 12 | cbvabv 2811 |
. . . 4
⊢ {𝑔 ∣ ∃𝑑 ∈ 𝐵 (𝑔 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑔‘𝑥) = (𝐺‘〈𝑥, (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))〉))} = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
14 | 1, 13 | eqtr4i 2768 |
. . 3
⊢ 𝐶 = {𝑔 ∣ ∃𝑑 ∈ 𝐵 (𝑔 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑔‘𝑥) = (𝐺‘〈𝑥, (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))〉))} |
15 | 14 | bnj1436 32532 |
. 2
⊢ (𝑔 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 (𝑔 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑔‘𝑥) = (𝐺‘〈𝑥, (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))〉))) |
16 | | bnj1239 32498 |
. 2
⊢
(∃𝑑 ∈
𝐵 (𝑔 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑔‘𝑥) = (𝐺‘〈𝑥, (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))〉)) → ∃𝑑 ∈ 𝐵 𝑔 Fn 𝑑) |
17 | | fnrel 6480 |
. . 3
⊢ (𝑔 Fn 𝑑 → Rel 𝑔) |
18 | 17 | rexlimivw 3201 |
. 2
⊢
(∃𝑑 ∈
𝐵 𝑔 Fn 𝑑 → Rel 𝑔) |
19 | 15, 16, 18 | 3syl 18 |
1
⊢ (𝑔 ∈ 𝐶 → Rel 𝑔) |