Step | Hyp | Ref
| Expression |
1 | | bnj1501.5 |
. 2
⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴)) |
2 | 1 | simprbi 479 |
. . . . . . . 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 30384 |
. . . . . . . . . 10
⊢ (𝑅 FrSe 𝐴 → 𝐹 Fn 𝐴) |
8 | | fndm 5904 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 FrSe 𝐴 → dom 𝐹 = 𝐴) |
10 | 1, 9 | bnj832 30082 |
. . . . . . . 8
⊢ (𝜑 → dom 𝐹 = 𝐴) |
11 | 2, 10 | eleqtrrd 2691 |
. . . . . . 7
⊢ (𝜑 → 𝑥 ∈ dom 𝐹) |
12 | 6 | dmeqi 5247 |
. . . . . . . 8
⊢ dom 𝐹 = dom ∪ 𝐶 |
13 | 5 | bnj1317 30146 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝐶 → ∀𝑓 𝑤 ∈ 𝐶) |
14 | 13 | bnj1400 30160 |
. . . . . . . 8
⊢ dom ∪ 𝐶 =
∪ 𝑓 ∈ 𝐶 dom 𝑓 |
15 | 12, 14 | eqtri 2632 |
. . . . . . 7
⊢ dom 𝐹 = ∪ 𝑓 ∈ 𝐶 dom 𝑓 |
16 | 11, 15 | syl6eleq 2698 |
. . . . . 6
⊢ (𝜑 → 𝑥 ∈ ∪
𝑓 ∈ 𝐶 dom 𝑓) |
17 | 16 | bnj1405 30161 |
. . . . 5
⊢ (𝜑 → ∃𝑓 ∈ 𝐶 𝑥 ∈ dom 𝑓) |
18 | | bnj1501.6 |
. . . . 5
⊢ (𝜓 ↔ (𝜑 ∧ 𝑓 ∈ 𝐶 ∧ 𝑥 ∈ dom 𝑓)) |
19 | 17, 18 | bnj1209 30121 |
. . . 4
⊢ (𝜑 → ∃𝑓𝜓) |
20 | 5 | bnj1436 30164 |
. . . . . . . . . 10
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))) |
21 | 20 | bnj1299 30143 |
. . . . . . . . 9
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 𝑓 Fn 𝑑) |
22 | | fndm 5904 |
. . . . . . . . 9
⊢ (𝑓 Fn 𝑑 → dom 𝑓 = 𝑑) |
23 | 21, 22 | bnj31 30039 |
. . . . . . . 8
⊢ (𝑓 ∈ 𝐶 → ∃𝑑 ∈ 𝐵 dom 𝑓 = 𝑑) |
24 | 18, 23 | bnj836 30084 |
. . . . . . 7
⊢ (𝜓 → ∃𝑑 ∈ 𝐵 dom 𝑓 = 𝑑) |
25 | | bnj1501.7 |
. . . . . . 7
⊢ (𝜒 ↔ (𝜓 ∧ 𝑑 ∈ 𝐵 ∧ dom 𝑓 = 𝑑)) |
26 | 3, 4, 5, 6, 1, 18 | bnj1518 30386 |
. . . . . . 7
⊢ (𝜓 → ∀𝑑𝜓) |
27 | 24, 25, 26 | bnj1521 30175 |
. . . . . 6
⊢ (𝜓 → ∃𝑑𝜒) |
28 | 7 | bnj930 30094 |
. . . . . . . . . . . 12
⊢ (𝑅 FrSe 𝐴 → Fun 𝐹) |
29 | 1, 28 | bnj832 30082 |
. . . . . . . . . . 11
⊢ (𝜑 → Fun 𝐹) |
30 | 18, 29 | bnj835 30083 |
. . . . . . . . . 10
⊢ (𝜓 → Fun 𝐹) |
31 | | elssuni 4403 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ 𝐶 → 𝑓 ⊆ ∪ 𝐶) |
32 | 31, 6 | syl6sseqr 3615 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ 𝐶 → 𝑓 ⊆ 𝐹) |
33 | 18, 32 | bnj836 30084 |
. . . . . . . . . 10
⊢ (𝜓 → 𝑓 ⊆ 𝐹) |
34 | 18 | simp3bi 1071 |
. . . . . . . . . 10
⊢ (𝜓 → 𝑥 ∈ dom 𝑓) |
35 | 30, 33, 34 | bnj1502 30172 |
. . . . . . . . 9
⊢ (𝜓 → (𝐹‘𝑥) = (𝑓‘𝑥)) |
36 | 3, 4, 5 | bnj1514 30385 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ 𝐶 → ∀𝑥 ∈ dom 𝑓(𝑓‘𝑥) = (𝐺‘𝑌)) |
37 | 18, 36 | bnj836 30084 |
. . . . . . . . . 10
⊢ (𝜓 → ∀𝑥 ∈ dom 𝑓(𝑓‘𝑥) = (𝐺‘𝑌)) |
38 | 37, 34 | bnj1294 30142 |
. . . . . . . . 9
⊢ (𝜓 → (𝑓‘𝑥) = (𝐺‘𝑌)) |
39 | 35, 38 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝜓 → (𝐹‘𝑥) = (𝐺‘𝑌)) |
40 | 25, 39 | bnj835 30083 |
. . . . . . 7
⊢ (𝜒 → (𝐹‘𝑥) = (𝐺‘𝑌)) |
41 | 25, 30 | bnj835 30083 |
. . . . . . . . . . 11
⊢ (𝜒 → Fun 𝐹) |
42 | 25, 33 | bnj835 30083 |
. . . . . . . . . . 11
⊢ (𝜒 → 𝑓 ⊆ 𝐹) |
43 | 3 | bnj1517 30174 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ 𝐵 → ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑) |
44 | 25, 43 | bnj836 30084 |
. . . . . . . . . . . . 13
⊢ (𝜒 → ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑) |
45 | 25, 34 | bnj835 30083 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → 𝑥 ∈ dom 𝑓) |
46 | 25 | simp3bi 1071 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → dom 𝑓 = 𝑑) |
47 | 45, 46 | eleqtrd 2690 |
. . . . . . . . . . . . 13
⊢ (𝜒 → 𝑥 ∈ 𝑑) |
48 | 44, 47 | bnj1294 30142 |
. . . . . . . . . . . 12
⊢ (𝜒 → pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑) |
49 | 48, 46 | sseqtr4d 3605 |
. . . . . . . . . . 11
⊢ (𝜒 → pred(𝑥, 𝐴, 𝑅) ⊆ dom 𝑓) |
50 | 41, 42, 49 | bnj1503 30173 |
. . . . . . . . . 10
⊢ (𝜒 → (𝐹 ↾ pred(𝑥, 𝐴, 𝑅)) = (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))) |
51 | 50 | opeq2d 4347 |
. . . . . . . . 9
⊢ (𝜒 → 〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉) |
52 | 51, 4 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝜒 → 〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉 = 𝑌) |
53 | 52 | fveq2d 6107 |
. . . . . . 7
⊢ (𝜒 → (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉) = (𝐺‘𝑌)) |
54 | 40, 53 | eqtr4d 2647 |
. . . . . 6
⊢ (𝜒 → (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
55 | 27, 54 | bnj593 30069 |
. . . . 5
⊢ (𝜓 → ∃𝑑(𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
56 | 3, 4, 5, 6 | bnj1519 30387 |
. . . . 5
⊢ ((𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉) → ∀𝑑(𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
57 | 55, 56 | bnj1397 30159 |
. . . 4
⊢ (𝜓 → (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
58 | 19, 57 | bnj593 30069 |
. . 3
⊢ (𝜑 → ∃𝑓(𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
59 | 3, 4, 5, 6 | bnj1520 30388 |
. . 3
⊢ ((𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉) → ∀𝑓(𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
60 | 58, 59 | bnj1397 30159 |
. 2
⊢ (𝜑 → (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
61 | 1, 60 | bnj1459 30167 |
1
⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |