Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ ( 0 ..^ 0 ) = ( 0 ..^ 0 ) |
2 |
1
|
naryrcl |
⊢ ( 𝐹 ∈ ( 0 -aryF 𝑋 ) → ( 0 ∈ ℕ0 ∧ 𝑋 ∈ V ) ) |
3 |
|
0aryfvalel |
⊢ ( 𝑋 ∈ V → ( 𝐹 ∈ ( 0 -aryF 𝑋 ) ↔ ∃ 𝑥 ∈ 𝑋 𝐹 = { 〈 ∅ , 𝑥 〉 } ) ) |
4 |
|
0ex |
⊢ ∅ ∈ V |
5 |
|
fvsng |
⊢ ( ( ∅ ∈ V ∧ 𝑥 ∈ 𝑋 ) → ( { 〈 ∅ , 𝑥 〉 } ‘ ∅ ) = 𝑥 ) |
6 |
4 5
|
mpan |
⊢ ( 𝑥 ∈ 𝑋 → ( { 〈 ∅ , 𝑥 〉 } ‘ ∅ ) = 𝑥 ) |
7 |
|
fveq1 |
⊢ ( 𝐹 = { 〈 ∅ , 𝑥 〉 } → ( 𝐹 ‘ ∅ ) = ( { 〈 ∅ , 𝑥 〉 } ‘ ∅ ) ) |
8 |
7
|
eqeq1d |
⊢ ( 𝐹 = { 〈 ∅ , 𝑥 〉 } → ( ( 𝐹 ‘ ∅ ) = 𝑥 ↔ ( { 〈 ∅ , 𝑥 〉 } ‘ ∅ ) = 𝑥 ) ) |
9 |
6 8
|
syl5ibrcom |
⊢ ( 𝑥 ∈ 𝑋 → ( 𝐹 = { 〈 ∅ , 𝑥 〉 } → ( 𝐹 ‘ ∅ ) = 𝑥 ) ) |
10 |
9
|
reximia |
⊢ ( ∃ 𝑥 ∈ 𝑋 𝐹 = { 〈 ∅ , 𝑥 〉 } → ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ ∅ ) = 𝑥 ) |
11 |
3 10
|
syl6bi |
⊢ ( 𝑋 ∈ V → ( 𝐹 ∈ ( 0 -aryF 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ ∅ ) = 𝑥 ) ) |
12 |
11
|
adantl |
⊢ ( ( 0 ∈ ℕ0 ∧ 𝑋 ∈ V ) → ( 𝐹 ∈ ( 0 -aryF 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ ∅ ) = 𝑥 ) ) |
13 |
2 12
|
mpcom |
⊢ ( 𝐹 ∈ ( 0 -aryF 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐹 ‘ ∅ ) = 𝑥 ) |