Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1497.1 |
⊢ 𝐵 = { 𝑑 ∣ ( 𝑑 ⊆ 𝐴 ∧ ∀ 𝑥 ∈ 𝑑 pred ( 𝑥 , 𝐴 , 𝑅 ) ⊆ 𝑑 ) } |
2 |
|
bnj1497.2 |
⊢ 𝑌 = 〈 𝑥 , ( 𝑓 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 |
3 |
|
bnj1497.3 |
⊢ 𝐶 = { 𝑓 ∣ ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) } |
4 |
3
|
bnj1317 |
⊢ ( 𝑔 ∈ 𝐶 → ∀ 𝑓 𝑔 ∈ 𝐶 ) |
5 |
4
|
nf5i |
⊢ Ⅎ 𝑓 𝑔 ∈ 𝐶 |
6 |
|
nfv |
⊢ Ⅎ 𝑓 Fun 𝑔 |
7 |
5 6
|
nfim |
⊢ Ⅎ 𝑓 ( 𝑔 ∈ 𝐶 → Fun 𝑔 ) |
8 |
|
eleq1w |
⊢ ( 𝑓 = 𝑔 → ( 𝑓 ∈ 𝐶 ↔ 𝑔 ∈ 𝐶 ) ) |
9 |
|
funeq |
⊢ ( 𝑓 = 𝑔 → ( Fun 𝑓 ↔ Fun 𝑔 ) ) |
10 |
8 9
|
imbi12d |
⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ∈ 𝐶 → Fun 𝑓 ) ↔ ( 𝑔 ∈ 𝐶 → Fun 𝑔 ) ) ) |
11 |
3
|
bnj1436 |
⊢ ( 𝑓 ∈ 𝐶 → ∃ 𝑑 ∈ 𝐵 ( 𝑓 Fn 𝑑 ∧ ∀ 𝑥 ∈ 𝑑 ( 𝑓 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑌 ) ) ) |
12 |
11
|
bnj1299 |
⊢ ( 𝑓 ∈ 𝐶 → ∃ 𝑑 ∈ 𝐵 𝑓 Fn 𝑑 ) |
13 |
|
fnfun |
⊢ ( 𝑓 Fn 𝑑 → Fun 𝑓 ) |
14 |
12 13
|
bnj31 |
⊢ ( 𝑓 ∈ 𝐶 → ∃ 𝑑 ∈ 𝐵 Fun 𝑓 ) |
15 |
14
|
bnj1265 |
⊢ ( 𝑓 ∈ 𝐶 → Fun 𝑓 ) |
16 |
7 10 15
|
chvarfv |
⊢ ( 𝑔 ∈ 𝐶 → Fun 𝑔 ) |
17 |
16
|
rgen |
⊢ ∀ 𝑔 ∈ 𝐶 Fun 𝑔 |