Step | Hyp | Ref
| Expression |
1 | | bnj1280.1 |
. . . . . . . 8
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} |
2 | | bnj1280.2 |
. . . . . . . 8
⊢ 𝑌 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
3 | | bnj1280.3 |
. . . . . . . 8
⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
4 | | bnj1280.4 |
. . . . . . . 8
⊢ 𝐷 = (dom 𝑔 ∩ dom ℎ) |
5 | | bnj1280.5 |
. . . . . . . 8
⊢ 𝐸 = {𝑥 ∈ 𝐷 ∣ (𝑔‘𝑥) ≠ (ℎ‘𝑥)} |
6 | | bnj1280.6 |
. . . . . . . 8
⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑔 ∈ 𝐶 ∧ ℎ ∈ 𝐶 ∧ (𝑔 ↾ 𝐷) ≠ (ℎ ↾ 𝐷))) |
7 | | bnj1280.7 |
. . . . . . . 8
⊢ (𝜓 ↔ (𝜑 ∧ 𝑥 ∈ 𝐸 ∧ ∀𝑦 ∈ 𝐸 ¬ 𝑦𝑅𝑥)) |
8 | 1, 2, 3, 4, 5, 6, 7 | bnj1286 32582 |
. . . . . . 7
⊢ (𝜓 → pred(𝑥, 𝐴, 𝑅) ⊆ 𝐷) |
9 | 8 | sseld 3886 |
. . . . . 6
⊢ (𝜓 → (𝑧 ∈ pred(𝑥, 𝐴, 𝑅) → 𝑧 ∈ 𝐷)) |
10 | | bnj1280.17 |
. . . . . . . . 9
⊢ (𝜓 → ( pred(𝑥, 𝐴, 𝑅) ∩ 𝐸) = ∅) |
11 | | disj1 4350 |
. . . . . . . . 9
⊢ ((
pred(𝑥, 𝐴, 𝑅) ∩ 𝐸) = ∅ ↔ ∀𝑧(𝑧 ∈ pred(𝑥, 𝐴, 𝑅) → ¬ 𝑧 ∈ 𝐸)) |
12 | 10, 11 | sylib 221 |
. . . . . . . 8
⊢ (𝜓 → ∀𝑧(𝑧 ∈ pred(𝑥, 𝐴, 𝑅) → ¬ 𝑧 ∈ 𝐸)) |
13 | 12 | 19.21bi 2190 |
. . . . . . 7
⊢ (𝜓 → (𝑧 ∈ pred(𝑥, 𝐴, 𝑅) → ¬ 𝑧 ∈ 𝐸)) |
14 | | fveq2 6686 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (𝑔‘𝑥) = (𝑔‘𝑧)) |
15 | | fveq2 6686 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (ℎ‘𝑥) = (ℎ‘𝑧)) |
16 | 14, 15 | neeq12d 2996 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → ((𝑔‘𝑥) ≠ (ℎ‘𝑥) ↔ (𝑔‘𝑧) ≠ (ℎ‘𝑧))) |
17 | 16, 5 | elrab2 3596 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐸 ↔ (𝑧 ∈ 𝐷 ∧ (𝑔‘𝑧) ≠ (ℎ‘𝑧))) |
18 | 17 | notbii 323 |
. . . . . . . 8
⊢ (¬
𝑧 ∈ 𝐸 ↔ ¬ (𝑧 ∈ 𝐷 ∧ (𝑔‘𝑧) ≠ (ℎ‘𝑧))) |
19 | | imnan 403 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐷 → ¬ (𝑔‘𝑧) ≠ (ℎ‘𝑧)) ↔ ¬ (𝑧 ∈ 𝐷 ∧ (𝑔‘𝑧) ≠ (ℎ‘𝑧))) |
20 | | nne 2939 |
. . . . . . . . 9
⊢ (¬
(𝑔‘𝑧) ≠ (ℎ‘𝑧) ↔ (𝑔‘𝑧) = (ℎ‘𝑧)) |
21 | 20 | imbi2i 339 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐷 → ¬ (𝑔‘𝑧) ≠ (ℎ‘𝑧)) ↔ (𝑧 ∈ 𝐷 → (𝑔‘𝑧) = (ℎ‘𝑧))) |
22 | 18, 19, 21 | 3bitr2i 302 |
. . . . . . 7
⊢ (¬
𝑧 ∈ 𝐸 ↔ (𝑧 ∈ 𝐷 → (𝑔‘𝑧) = (ℎ‘𝑧))) |
23 | 13, 22 | syl6ib 254 |
. . . . . 6
⊢ (𝜓 → (𝑧 ∈ pred(𝑥, 𝐴, 𝑅) → (𝑧 ∈ 𝐷 → (𝑔‘𝑧) = (ℎ‘𝑧)))) |
24 | 9, 23 | mpdd 43 |
. . . . 5
⊢ (𝜓 → (𝑧 ∈ pred(𝑥, 𝐴, 𝑅) → (𝑔‘𝑧) = (ℎ‘𝑧))) |
25 | 24 | imp 410 |
. . . 4
⊢ ((𝜓 ∧ 𝑧 ∈ pred(𝑥, 𝐴, 𝑅)) → (𝑔‘𝑧) = (ℎ‘𝑧)) |
26 | | fvres 6705 |
. . . . . 6
⊢ (𝑧 ∈ 𝐷 → ((𝑔 ↾ 𝐷)‘𝑧) = (𝑔‘𝑧)) |
27 | 9, 26 | syl6 35 |
. . . . 5
⊢ (𝜓 → (𝑧 ∈ pred(𝑥, 𝐴, 𝑅) → ((𝑔 ↾ 𝐷)‘𝑧) = (𝑔‘𝑧))) |
28 | 27 | imp 410 |
. . . 4
⊢ ((𝜓 ∧ 𝑧 ∈ pred(𝑥, 𝐴, 𝑅)) → ((𝑔 ↾ 𝐷)‘𝑧) = (𝑔‘𝑧)) |
29 | | fvres 6705 |
. . . . . 6
⊢ (𝑧 ∈ 𝐷 → ((ℎ ↾ 𝐷)‘𝑧) = (ℎ‘𝑧)) |
30 | 9, 29 | syl6 35 |
. . . . 5
⊢ (𝜓 → (𝑧 ∈ pred(𝑥, 𝐴, 𝑅) → ((ℎ ↾ 𝐷)‘𝑧) = (ℎ‘𝑧))) |
31 | 30 | imp 410 |
. . . 4
⊢ ((𝜓 ∧ 𝑧 ∈ pred(𝑥, 𝐴, 𝑅)) → ((ℎ ↾ 𝐷)‘𝑧) = (ℎ‘𝑧)) |
32 | 25, 28, 31 | 3eqtr4d 2784 |
. . 3
⊢ ((𝜓 ∧ 𝑧 ∈ pred(𝑥, 𝐴, 𝑅)) → ((𝑔 ↾ 𝐷)‘𝑧) = ((ℎ ↾ 𝐷)‘𝑧)) |
33 | 32 | ralrimiva 3097 |
. 2
⊢ (𝜓 → ∀𝑧 ∈ pred (𝑥, 𝐴, 𝑅)((𝑔 ↾ 𝐷)‘𝑧) = ((ℎ ↾ 𝐷)‘𝑧)) |
34 | 8 | resabs1d 5866 |
. . . 4
⊢ (𝜓 → ((𝑔 ↾ 𝐷) ↾ pred(𝑥, 𝐴, 𝑅)) = (𝑔 ↾ pred(𝑥, 𝐴, 𝑅))) |
35 | 8 | resabs1d 5866 |
. . . 4
⊢ (𝜓 → ((ℎ ↾ 𝐷) ↾ pred(𝑥, 𝐴, 𝑅)) = (ℎ ↾ pred(𝑥, 𝐴, 𝑅))) |
36 | 34, 35 | eqeq12d 2755 |
. . 3
⊢ (𝜓 → (((𝑔 ↾ 𝐷) ↾ pred(𝑥, 𝐴, 𝑅)) = ((ℎ ↾ 𝐷) ↾ pred(𝑥, 𝐴, 𝑅)) ↔ (𝑔 ↾ pred(𝑥, 𝐴, 𝑅)) = (ℎ ↾ pred(𝑥, 𝐴, 𝑅)))) |
37 | 1, 2, 3, 4, 5, 6, 7 | bnj1256 32578 |
. . . . . . 7
⊢ (𝜑 → ∃𝑑 ∈ 𝐵 𝑔 Fn 𝑑) |
38 | 4 | bnj1292 32378 |
. . . . . . . . 9
⊢ 𝐷 ⊆ dom 𝑔 |
39 | | fndm 6450 |
. . . . . . . . 9
⊢ (𝑔 Fn 𝑑 → dom 𝑔 = 𝑑) |
40 | 38, 39 | sseqtrid 3939 |
. . . . . . . 8
⊢ (𝑔 Fn 𝑑 → 𝐷 ⊆ 𝑑) |
41 | | fnssres 6469 |
. . . . . . . 8
⊢ ((𝑔 Fn 𝑑 ∧ 𝐷 ⊆ 𝑑) → (𝑔 ↾ 𝐷) Fn 𝐷) |
42 | 40, 41 | mpdan 687 |
. . . . . . 7
⊢ (𝑔 Fn 𝑑 → (𝑔 ↾ 𝐷) Fn 𝐷) |
43 | 37, 42 | bnj31 32280 |
. . . . . 6
⊢ (𝜑 → ∃𝑑 ∈ 𝐵 (𝑔 ↾ 𝐷) Fn 𝐷) |
44 | 43 | bnj1265 32375 |
. . . . 5
⊢ (𝜑 → (𝑔 ↾ 𝐷) Fn 𝐷) |
45 | 7, 44 | bnj835 32321 |
. . . 4
⊢ (𝜓 → (𝑔 ↾ 𝐷) Fn 𝐷) |
46 | 1, 2, 3, 4, 5, 6, 7 | bnj1259 32579 |
. . . . . . 7
⊢ (𝜑 → ∃𝑑 ∈ 𝐵 ℎ Fn 𝑑) |
47 | 4 | bnj1293 32379 |
. . . . . . . . 9
⊢ 𝐷 ⊆ dom ℎ |
48 | | fndm 6450 |
. . . . . . . . 9
⊢ (ℎ Fn 𝑑 → dom ℎ = 𝑑) |
49 | 47, 48 | sseqtrid 3939 |
. . . . . . . 8
⊢ (ℎ Fn 𝑑 → 𝐷 ⊆ 𝑑) |
50 | | fnssres 6469 |
. . . . . . . 8
⊢ ((ℎ Fn 𝑑 ∧ 𝐷 ⊆ 𝑑) → (ℎ ↾ 𝐷) Fn 𝐷) |
51 | 49, 50 | mpdan 687 |
. . . . . . 7
⊢ (ℎ Fn 𝑑 → (ℎ ↾ 𝐷) Fn 𝐷) |
52 | 46, 51 | bnj31 32280 |
. . . . . 6
⊢ (𝜑 → ∃𝑑 ∈ 𝐵 (ℎ ↾ 𝐷) Fn 𝐷) |
53 | 52 | bnj1265 32375 |
. . . . 5
⊢ (𝜑 → (ℎ ↾ 𝐷) Fn 𝐷) |
54 | 7, 53 | bnj835 32321 |
. . . 4
⊢ (𝜓 → (ℎ ↾ 𝐷) Fn 𝐷) |
55 | | fvreseq 6829 |
. . . 4
⊢ ((((𝑔 ↾ 𝐷) Fn 𝐷 ∧ (ℎ ↾ 𝐷) Fn 𝐷) ∧ pred(𝑥, 𝐴, 𝑅) ⊆ 𝐷) → (((𝑔 ↾ 𝐷) ↾ pred(𝑥, 𝐴, 𝑅)) = ((ℎ ↾ 𝐷) ↾ pred(𝑥, 𝐴, 𝑅)) ↔ ∀𝑧 ∈ pred (𝑥, 𝐴, 𝑅)((𝑔 ↾ 𝐷)‘𝑧) = ((ℎ ↾ 𝐷)‘𝑧))) |
56 | 45, 54, 8, 55 | syl21anc 837 |
. . 3
⊢ (𝜓 → (((𝑔 ↾ 𝐷) ↾ pred(𝑥, 𝐴, 𝑅)) = ((ℎ ↾ 𝐷) ↾ pred(𝑥, 𝐴, 𝑅)) ↔ ∀𝑧 ∈ pred (𝑥, 𝐴, 𝑅)((𝑔 ↾ 𝐷)‘𝑧) = ((ℎ ↾ 𝐷)‘𝑧))) |
57 | 36, 56 | bitr3d 284 |
. 2
⊢ (𝜓 → ((𝑔 ↾ pred(𝑥, 𝐴, 𝑅)) = (ℎ ↾ pred(𝑥, 𝐴, 𝑅)) ↔ ∀𝑧 ∈ pred (𝑥, 𝐴, 𝑅)((𝑔 ↾ 𝐷)‘𝑧) = ((ℎ ↾ 𝐷)‘𝑧))) |
58 | 33, 57 | mpbird 260 |
1
⊢ (𝜓 → (𝑔 ↾ pred(𝑥, 𝐴, 𝑅)) = (ℎ ↾ pred(𝑥, 𝐴, 𝑅))) |