Step | Hyp | Ref
| Expression |
1 | | bnj1501.5 |
. 2
⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴)) |
2 | 1 | simprbi 480 |
. . . . . . . 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 31130 |
. . . . . . . . . 10
⊢ (𝑅 FrSe 𝐴 → 𝐹 Fn 𝐴) |
8 | | fndm 5990 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 FrSe 𝐴 → dom 𝐹 = 𝐴) |
10 | 1, 9 | bnj832 30828 |
. . . . . . . 8
⊢ (𝜑 → dom 𝐹 = 𝐴) |
11 | 2, 10 | eleqtrrd 2704 |
. . . . . . 7
⊢ (𝜑 → 𝑥 ∈ dom 𝐹) |
12 | 6 | dmeqi 5325 |
. . . . . . . 8
⊢ dom 𝐹 = dom ∪ 𝐶 |
13 | 5 | bnj1317 30892 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐶 → ∀𝑓 𝑤 ∈ 𝐶) |
14 | 13 | bnj1400 30906 |
. . . . . . . 8
⊢ dom ∪ 𝐶 =
∪ 𝑓 ∈ 𝐶 dom 𝑓 |
15 | 12, 14 | eqtri 2644 |
. . . . . . 7
⊢ dom 𝐹 = ∪ 𝑓 ∈ 𝐶 dom 𝑓 |
16 | 11, 15 | syl6eleq 2711 |
. . . . . 6
⊢ (𝜑 → 𝑥 ∈ ∪
𝑓 ∈ 𝐶 dom 𝑓) |
17 | 16 | bnj1405 30907 |
. . . . 5
⊢ (𝜑 → ∃𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓) |
18 | | bnj1501.6 |
. . . . 5
⊢ (𝜓 ↔ (𝜑 ∧ 𝑓 ∈ 𝐶 ∧ 𝑥 ∈ dom 𝑓)) |
19 | 17, 18 | bnj1209 30867 |
. . . 4
⊢ (𝜑 → ∃𝑓𝜓) |
20 | 5 | bnj1436 30910 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))) |
21 | 20 | bnj1299 30889 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 𝑓 Fn 𝑑) |
22 | | fndm 5990 |
. . . . . . . . 9
⊢ (𝑓 Fn 𝑑 → dom 𝑓 = 𝑑) |
23 | 21, 22 | bnj31 30785 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 dom 𝑓 = 𝑑) |
24 | 18, 23 | bnj836 30830 |
. . . . . . 7
⊢ (𝜓 → ∃𝑑 ∈ 𝐵 dom 𝑓 = 𝑑) |
25 | | bnj1501.7 |
. . . . . . 7
⊢ (𝜒 ↔ (𝜓 ∧ 𝑑 ∈ 𝐵 ∧ dom 𝑓 = 𝑑)) |
26 | 3, 4, 5, 6, 1, 18 | bnj1518 31132 |
. . . . . . 7
⊢ (𝜓 → ∀𝑑𝜓) |
27 | 24, 25, 26 | bnj1521 30921 |
. . . . . 6
⊢ (𝜓 → ∃𝑑𝜒) |
28 | 7 | bnj930 30840 |
. . . . . . . . . . . 12
⊢ (𝑅 FrSe 𝐴 → Fun 𝐹) |
29 | 1, 28 | bnj832 30828 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐹) |
30 | 18, 29 | bnj835 30829 |
. . . . . . . . . 10
⊢ (𝜓 → Fun 𝐹) |
31 | | elssuni 4467 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ 𝐶 → 𝑓 ⊆ ∪ 𝐶) |
32 | 31, 6 | syl6sseqr 3652 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ 𝐶 → 𝑓 ⊆ 𝐹) |
33 | 18, 32 | bnj836 30830 |
. . . . . . . . . 10
⊢ (𝜓 → 𝑓 ⊆ 𝐹) |
34 | 18 | simp3bi 1078 |
. . . . . . . . . 10
⊢ (𝜓 → 𝑥 ∈ dom 𝑓) |
35 | 30, 33, 34 | bnj1502 30918 |
. . . . . . . . 9
⊢ (𝜓 → (𝐹‘𝑥) = (𝑓‘𝑥)) |
36 | 3, 4, 5 | bnj1514 31131 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ 𝐶 → ∀𝑥 ∈ dom 𝑓(𝑓‘𝑥) = (𝐺‘𝑌)) |
37 | 18, 36 | bnj836 30830 |
. . . . . . . . . 10
⊢ (𝜓 → ∀𝑥 ∈ dom 𝑓(𝑓‘𝑥) = (𝐺‘𝑌)) |
38 | 37, 34 | bnj1294 30888 |
. . . . . . . . 9
⊢ (𝜓 → (𝑓‘𝑥) = (𝐺‘𝑌)) |
39 | 35, 38 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝜓 → (𝐹‘𝑥) = (𝐺‘𝑌)) |
40 | 25, 39 | bnj835 30829 |
. . . . . . 7
⊢ (𝜒 → (𝐹‘𝑥) = (𝐺‘𝑌)) |
41 | 25, 30 | bnj835 30829 |
. . . . . . . . . . 11
⊢ (𝜒 → Fun 𝐹) |
42 | 25, 33 | bnj835 30829 |
. . . . . . . . . . 11
⊢ (𝜒 → 𝑓 ⊆ 𝐹) |
43 | 3 | bnj1517 30920 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ 𝐵 → ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑) |
44 | 25, 43 | bnj836 30830 |
. . . . . . . . . . . . 13
⊢ (𝜒 → ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑) |
45 | 25, 34 | bnj835 30829 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → 𝑥 ∈ dom 𝑓) |
46 | 25 | simp3bi 1078 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → dom 𝑓 = 𝑑) |
47 | 45, 46 | eleqtrd 2703 |
. . . . . . . . . . . . 13
⊢ (𝜒 → 𝑥 ∈ 𝑑) |
48 | 44, 47 | bnj1294 30888 |
. . . . . . . . . . . 12
⊢ (𝜒 → pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑) |
49 | 48, 46 | sseqtr4d 3642 |
. . . . . . . . . . 11
⊢ (𝜒 → pred(𝑥, 𝐴, 𝑅) ⊆ dom 𝑓) |
50 | 41, 42, 49 | bnj1503 30919 |
. . . . . . . . . 10
⊢ (𝜒 → (𝐹 ↾ pred(𝑥, 𝐴, 𝑅)) = (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))) |
51 | 50 | opeq2d 4409 |
. . . . . . . . 9
⊢ (𝜒 → 〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉) |
52 | 51, 4 | syl6eqr 2674 |
. . . . . . . 8
⊢ (𝜒 → 〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉 = 𝑌) |
53 | 52 | fveq2d 6195 |
. . . . . . 7
⊢ (𝜒 → (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉) = (𝐺‘𝑌)) |
54 | 40, 53 | eqtr4d 2659 |
. . . . . 6
⊢ (𝜒 → (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
55 | 27, 54 | bnj593 30815 |
. . . . 5
⊢ (𝜓 → ∃𝑑(𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
56 | 3, 4, 5, 6 | bnj1519 31133 |
. . . . 5
⊢ ((𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉) → ∀𝑑(𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
57 | 55, 56 | bnj1397 30905 |
. . . 4
⊢ (𝜓 → (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
58 | 19, 57 | bnj593 30815 |
. . 3
⊢ (𝜑 → ∃𝑓(𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
59 | 3, 4, 5, 6 | bnj1520 31134 |
. . 3
⊢ ((𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉) → ∀𝑓(𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
60 | 58, 59 | bnj1397 30905 |
. 2
⊢ (𝜑 → (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
61 | 1, 60 | bnj1459 30913 |
1
⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |