Step | Hyp | Ref
| Expression |
1 | | bnj1501.5 |
. 2
⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴)) |
2 | 1 | simprbi 498 |
. . . . . . . 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 34073 |
. . . . . . . . . 10
⊢ (𝑅 FrSe 𝐴 → 𝐹 Fn 𝐴) |
8 | 7 | fndmd 6655 |
. . . . . . . . 9
⊢ (𝑅 FrSe 𝐴 → dom 𝐹 = 𝐴) |
9 | 1, 8 | bnj832 33769 |
. . . . . . . 8
⊢ (𝜑 → dom 𝐹 = 𝐴) |
10 | 2, 9 | eleqtrrd 2837 |
. . . . . . 7
⊢ (𝜑 → 𝑥 ∈ dom 𝐹) |
11 | 6 | dmeqi 5905 |
. . . . . . . 8
⊢ dom 𝐹 = dom ∪ 𝐶 |
12 | 5 | bnj1317 33832 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐶 → ∀𝑓 𝑤 ∈ 𝐶) |
13 | 12 | bnj1400 33846 |
. . . . . . . 8
⊢ dom ∪ 𝐶 =
∪ 𝑓 ∈ 𝐶 dom 𝑓 |
14 | 11, 13 | eqtri 2761 |
. . . . . . 7
⊢ dom 𝐹 = ∪ 𝑓 ∈ 𝐶 dom 𝑓 |
15 | 10, 14 | eleqtrdi 2844 |
. . . . . 6
⊢ (𝜑 → 𝑥 ∈ ∪
𝑓 ∈ 𝐶 dom 𝑓) |
16 | 15 | bnj1405 33847 |
. . . . 5
⊢ (𝜑 → ∃𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓) |
17 | | bnj1501.6 |
. . . . 5
⊢ (𝜓 ↔ (𝜑 ∧ 𝑓 ∈ 𝐶 ∧ 𝑥 ∈ dom 𝑓)) |
18 | 16, 17 | bnj1209 33807 |
. . . 4
⊢ (𝜑 → ∃𝑓𝜓) |
19 | 5 | bnj1436 33850 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))) |
20 | 19 | bnj1299 33829 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 𝑓 Fn 𝑑) |
21 | | fndm 6653 |
. . . . . . . . 9
⊢ (𝑓 Fn 𝑑 → dom 𝑓 = 𝑑) |
22 | 20, 21 | bnj31 33730 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 dom 𝑓 = 𝑑) |
23 | 17, 22 | bnj836 33771 |
. . . . . . 7
⊢ (𝜓 → ∃𝑑 ∈ 𝐵 dom 𝑓 = 𝑑) |
24 | | bnj1501.7 |
. . . . . . 7
⊢ (𝜒 ↔ (𝜓 ∧ 𝑑 ∈ 𝐵 ∧ dom 𝑓 = 𝑑)) |
25 | 3, 4, 5, 6, 1, 17 | bnj1518 34075 |
. . . . . . 7
⊢ (𝜓 → ∀𝑑𝜓) |
26 | 23, 24, 25 | bnj1521 33862 |
. . . . . 6
⊢ (𝜓 → ∃𝑑𝜒) |
27 | 7 | fnfund 6651 |
. . . . . . . . . . . 12
⊢ (𝑅 FrSe 𝐴 → Fun 𝐹) |
28 | 1, 27 | bnj832 33769 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐹) |
29 | 17, 28 | bnj835 33770 |
. . . . . . . . . 10
⊢ (𝜓 → Fun 𝐹) |
30 | | elssuni 4942 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ 𝐶 → 𝑓 ⊆ ∪ 𝐶) |
31 | 30, 6 | sseqtrrdi 4034 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ 𝐶 → 𝑓 ⊆ 𝐹) |
32 | 17, 31 | bnj836 33771 |
. . . . . . . . . 10
⊢ (𝜓 → 𝑓 ⊆ 𝐹) |
33 | 17 | simp3bi 1148 |
. . . . . . . . . 10
⊢ (𝜓 → 𝑥 ∈ dom 𝑓) |
34 | 29, 32, 33 | bnj1502 33859 |
. . . . . . . . 9
⊢ (𝜓 → (𝐹‘𝑥) = (𝑓‘𝑥)) |
35 | 3, 4, 5 | bnj1514 34074 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ 𝐶 → ∀𝑥 ∈ dom 𝑓(𝑓‘𝑥) = (𝐺‘𝑌)) |
36 | 17, 35 | bnj836 33771 |
. . . . . . . . . 10
⊢ (𝜓 → ∀𝑥 ∈ dom 𝑓(𝑓‘𝑥) = (𝐺‘𝑌)) |
37 | 36, 33 | bnj1294 33828 |
. . . . . . . . 9
⊢ (𝜓 → (𝑓‘𝑥) = (𝐺‘𝑌)) |
38 | 34, 37 | eqtrd 2773 |
. . . . . . . 8
⊢ (𝜓 → (𝐹‘𝑥) = (𝐺‘𝑌)) |
39 | 24, 38 | bnj835 33770 |
. . . . . . 7
⊢ (𝜒 → (𝐹‘𝑥) = (𝐺‘𝑌)) |
40 | 24, 29 | bnj835 33770 |
. . . . . . . . . . 11
⊢ (𝜒 → Fun 𝐹) |
41 | 24, 32 | bnj835 33770 |
. . . . . . . . . . 11
⊢ (𝜒 → 𝑓 ⊆ 𝐹) |
42 | 3 | bnj1517 33861 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ 𝐵 → ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑) |
43 | 24, 42 | bnj836 33771 |
. . . . . . . . . . . . 13
⊢ (𝜒 → ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑) |
44 | 24, 33 | bnj835 33770 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → 𝑥 ∈ dom 𝑓) |
45 | 24 | simp3bi 1148 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → dom 𝑓 = 𝑑) |
46 | 44, 45 | eleqtrd 2836 |
. . . . . . . . . . . . 13
⊢ (𝜒 → 𝑥 ∈ 𝑑) |
47 | 43, 46 | bnj1294 33828 |
. . . . . . . . . . . 12
⊢ (𝜒 → pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑) |
48 | 47, 45 | sseqtrrd 4024 |
. . . . . . . . . . 11
⊢ (𝜒 → pred(𝑥, 𝐴, 𝑅) ⊆ dom 𝑓) |
49 | 40, 41, 48 | bnj1503 33860 |
. . . . . . . . . 10
⊢ (𝜒 → (𝐹 ↾ pred(𝑥, 𝐴, 𝑅)) = (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))) |
50 | 49 | opeq2d 4881 |
. . . . . . . . 9
⊢ (𝜒 → ⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩ = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩) |
51 | 50, 4 | eqtr4di 2791 |
. . . . . . . 8
⊢ (𝜒 → ⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩ = 𝑌) |
52 | 51 | fveq2d 6896 |
. . . . . . 7
⊢ (𝜒 → (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩) = (𝐺‘𝑌)) |
53 | 39, 52 | eqtr4d 2776 |
. . . . . 6
⊢ (𝜒 → (𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) |
54 | 26, 53 | bnj593 33756 |
. . . . 5
⊢ (𝜓 → ∃𝑑(𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) |
55 | 3, 4, 5, 6 | bnj1519 34076 |
. . . . 5
⊢ ((𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩) → ∀𝑑(𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) |
56 | 54, 55 | bnj1397 33845 |
. . . 4
⊢ (𝜓 → (𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) |
57 | 18, 56 | bnj593 33756 |
. . 3
⊢ (𝜑 → ∃𝑓(𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) |
58 | 3, 4, 5, 6 | bnj1520 34077 |
. . 3
⊢ ((𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩) → ∀𝑓(𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) |
59 | 57, 58 | bnj1397 33845 |
. 2
⊢ (𝜑 → (𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) |
60 | 1, 59 | bnj1459 33854 |
1
⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘⟨𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))⟩)) |