Step | Hyp | Ref
| Expression |
1 | | bnj1501.5 |
. 2
⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴)) |
2 | 1 | simprbi 495 |
. . . . . . . 8
⊢ (𝜑 → 𝑥 ∈ 𝐴) |
3 | | bnj1501.1 |
. . . . . . . . . . 11
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} |
4 | | bnj1501.2 |
. . . . . . . . . . 11
⊢ 𝑌 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
5 | | bnj1501.3 |
. . . . . . . . . . 11
⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
6 | | bnj1501.4 |
. . . . . . . . . . 11
⊢ 𝐹 = ∪
𝐶 |
7 | 3, 4, 5, 6 | bnj60 34826 |
. . . . . . . . . 10
⊢ (𝑅 FrSe 𝐴 → 𝐹 Fn 𝐴) |
8 | 7 | fndmd 6660 |
. . . . . . . . 9
⊢ (𝑅 FrSe 𝐴 → dom 𝐹 = 𝐴) |
9 | 1, 8 | bnj832 34522 |
. . . . . . . 8
⊢ (𝜑 → dom 𝐹 = 𝐴) |
10 | 2, 9 | eleqtrrd 2828 |
. . . . . . 7
⊢ (𝜑 → 𝑥 ∈ dom 𝐹) |
11 | 6 | dmeqi 5907 |
. . . . . . . 8
⊢ dom 𝐹 = dom ∪ 𝐶 |
12 | 5 | bnj1317 34585 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐶 → ∀𝑓 𝑤 ∈ 𝐶) |
13 | 12 | bnj1400 34599 |
. . . . . . . 8
⊢ dom ∪ 𝐶 =
∪ 𝑓 ∈ 𝐶 dom 𝑓 |
14 | 11, 13 | eqtri 2753 |
. . . . . . 7
⊢ dom 𝐹 = ∪ 𝑓 ∈ 𝐶 dom 𝑓 |
15 | 10, 14 | eleqtrdi 2835 |
. . . . . 6
⊢ (𝜑 → 𝑥 ∈ ∪
𝑓 ∈ 𝐶 dom 𝑓) |
16 | 15 | bnj1405 34600 |
. . . . 5
⊢ (𝜑 → ∃𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓) |
17 | | bnj1501.6 |
. . . . 5
⊢ (𝜓 ↔ (𝜑 ∧ 𝑓 ∈ 𝐶 ∧ 𝑥 ∈ dom 𝑓)) |
18 | 16, 17 | bnj1209 34560 |
. . . 4
⊢ (𝜑 → ∃𝑓𝜓) |
19 | 5 | bnj1436 34603 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))) |
20 | 19 | bnj1299 34582 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 𝑓 Fn 𝑑) |
21 | | fndm 6658 |
. . . . . . . . 9
⊢ (𝑓 Fn 𝑑 → dom 𝑓 = 𝑑) |
22 | 20, 21 | bnj31 34483 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 dom 𝑓 = 𝑑) |
23 | 17, 22 | bnj836 34524 |
. . . . . . 7
⊢ (𝜓 → ∃𝑑 ∈ 𝐵 dom 𝑓 = 𝑑) |
24 | | bnj1501.7 |
. . . . . . 7
⊢ (𝜒 ↔ (𝜓 ∧ 𝑑 ∈ 𝐵 ∧ dom 𝑓 = 𝑑)) |
25 | 3, 4, 5, 6, 1, 17 | bnj1518 34828 |
. . . . . . 7
⊢ (𝜓 → ∀𝑑𝜓) |
26 | 23, 24, 25 | bnj1521 34615 |
. . . . . 6
⊢ (𝜓 → ∃𝑑𝜒) |
27 | 7 | fnfund 6656 |
. . . . . . . . . . . 12
⊢ (𝑅 FrSe 𝐴 → Fun 𝐹) |
28 | 1, 27 | bnj832 34522 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐹) |
29 | 17, 28 | bnj835 34523 |
. . . . . . . . . 10
⊢ (𝜓 → Fun 𝐹) |
30 | | elssuni 4941 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ 𝐶 → 𝑓 ⊆ ∪ 𝐶) |
31 | 30, 6 | sseqtrrdi 4028 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ 𝐶 → 𝑓 ⊆ 𝐹) |
32 | 17, 31 | bnj836 34524 |
. . . . . . . . . 10
⊢ (𝜓 → 𝑓 ⊆ 𝐹) |
33 | 17 | simp3bi 1144 |
. . . . . . . . . 10
⊢ (𝜓 → 𝑥 ∈ dom 𝑓) |
34 | 29, 32, 33 | bnj1502 34612 |
. . . . . . . . 9
⊢ (𝜓 → (𝐹‘𝑥) = (𝑓‘𝑥)) |
35 | 3, 4, 5 | bnj1514 34827 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ 𝐶 → ∀𝑥 ∈ dom 𝑓(𝑓‘𝑥) = (𝐺‘𝑌)) |
36 | 17, 35 | bnj836 34524 |
. . . . . . . . . 10
⊢ (𝜓 → ∀𝑥 ∈ dom 𝑓(𝑓‘𝑥) = (𝐺‘𝑌)) |
37 | 36, 33 | bnj1294 34581 |
. . . . . . . . 9
⊢ (𝜓 → (𝑓‘𝑥) = (𝐺‘𝑌)) |
38 | 34, 37 | eqtrd 2765 |
. . . . . . . 8
⊢ (𝜓 → (𝐹‘𝑥) = (𝐺‘𝑌)) |
39 | 24, 38 | bnj835 34523 |
. . . . . . 7
⊢ (𝜒 → (𝐹‘𝑥) = (𝐺‘𝑌)) |
40 | 24, 29 | bnj835 34523 |
. . . . . . . . . . 11
⊢ (𝜒 → Fun 𝐹) |
41 | 24, 32 | bnj835 34523 |
. . . . . . . . . . 11
⊢ (𝜒 → 𝑓 ⊆ 𝐹) |
42 | 3 | bnj1517 34614 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ 𝐵 → ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑) |
43 | 24, 42 | bnj836 34524 |
. . . . . . . . . . . . 13
⊢ (𝜒 → ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑) |
44 | 24, 33 | bnj835 34523 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → 𝑥 ∈ dom 𝑓) |
45 | 24 | simp3bi 1144 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → dom 𝑓 = 𝑑) |
46 | 44, 45 | eleqtrd 2827 |
. . . . . . . . . . . . 13
⊢ (𝜒 → 𝑥 ∈ 𝑑) |
47 | 43, 46 | bnj1294 34581 |
. . . . . . . . . . . 12
⊢ (𝜒 → pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑) |
48 | 47, 45 | sseqtrrd 4018 |
. . . . . . . . . . 11
⊢ (𝜒 → pred(𝑥, 𝐴, 𝑅) ⊆ dom 𝑓) |
49 | 40, 41, 48 | bnj1503 34613 |
. . . . . . . . . 10
⊢ (𝜒 → (𝐹 ↾ pred(𝑥, 𝐴, 𝑅)) = (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))) |
50 | 49 | opeq2d 4882 |
. . . . . . . . 9
⊢ (𝜒 → 〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉) |
51 | 50, 4 | eqtr4di 2783 |
. . . . . . . 8
⊢ (𝜒 → 〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉 = 𝑌) |
52 | 51 | fveq2d 6900 |
. . . . . . 7
⊢ (𝜒 → (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉) = (𝐺‘𝑌)) |
53 | 39, 52 | eqtr4d 2768 |
. . . . . 6
⊢ (𝜒 → (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
54 | 26, 53 | bnj593 34509 |
. . . . 5
⊢ (𝜓 → ∃𝑑(𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
55 | 3, 4, 5, 6 | bnj1519 34829 |
. . . . 5
⊢ ((𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉) → ∀𝑑(𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
56 | 54, 55 | bnj1397 34598 |
. . . 4
⊢ (𝜓 → (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
57 | 18, 56 | bnj593 34509 |
. . 3
⊢ (𝜑 → ∃𝑓(𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
58 | 3, 4, 5, 6 | bnj1520 34830 |
. . 3
⊢ ((𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉) → ∀𝑓(𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
59 | 57, 58 | bnj1397 34598 |
. 2
⊢ (𝜑 → (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
60 | 1, 59 | bnj1459 34607 |
1
⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |