Step |
Hyp |
Ref |
Expression |
1 |
|
bnj96.1 |
⊢ 𝐹 = { 〈 ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) 〉 } |
2 |
|
bnj93 |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → pred ( 𝑥 , 𝐴 , 𝑅 ) ∈ V ) |
3 |
|
0ex |
⊢ ∅ ∈ V |
4 |
3
|
bnj519 |
⊢ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∈ V → Fun { 〈 ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) 〉 } ) |
5 |
1
|
funeqi |
⊢ ( Fun 𝐹 ↔ Fun { 〈 ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) 〉 } ) |
6 |
4 5
|
sylibr |
⊢ ( pred ( 𝑥 , 𝐴 , 𝑅 ) ∈ V → Fun 𝐹 ) |
7 |
2 6
|
syl |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → Fun 𝐹 ) |
8 |
|
opex |
⊢ 〈 ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) 〉 ∈ V |
9 |
8
|
snid |
⊢ 〈 ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) 〉 ∈ { 〈 ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) 〉 } |
10 |
9 1
|
eleqtrri |
⊢ 〈 ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) 〉 ∈ 𝐹 |
11 |
|
funopfv |
⊢ ( Fun 𝐹 → ( 〈 ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) 〉 ∈ 𝐹 → ( 𝐹 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) ) |
12 |
7 10 11
|
mpisyl |
⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) ) |