Step |
Hyp |
Ref |
Expression |
1 |
|
vafval.2 |
⊢ 𝐺 = ( +𝑣 ‘ 𝑈 ) |
2 |
|
df-va |
⊢ +𝑣 = ( 1st ∘ 1st ) |
3 |
2
|
fveq1i |
⊢ ( +𝑣 ‘ 𝑈 ) = ( ( 1st ∘ 1st ) ‘ 𝑈 ) |
4 |
|
fo1st |
⊢ 1st : V –onto→ V |
5 |
|
fof |
⊢ ( 1st : V –onto→ V → 1st : V ⟶ V ) |
6 |
4 5
|
ax-mp |
⊢ 1st : V ⟶ V |
7 |
|
fvco3 |
⊢ ( ( 1st : V ⟶ V ∧ 𝑈 ∈ V ) → ( ( 1st ∘ 1st ) ‘ 𝑈 ) = ( 1st ‘ ( 1st ‘ 𝑈 ) ) ) |
8 |
6 7
|
mpan |
⊢ ( 𝑈 ∈ V → ( ( 1st ∘ 1st ) ‘ 𝑈 ) = ( 1st ‘ ( 1st ‘ 𝑈 ) ) ) |
9 |
3 8
|
syl5eq |
⊢ ( 𝑈 ∈ V → ( +𝑣 ‘ 𝑈 ) = ( 1st ‘ ( 1st ‘ 𝑈 ) ) ) |
10 |
|
fvprc |
⊢ ( ¬ 𝑈 ∈ V → ( +𝑣 ‘ 𝑈 ) = ∅ ) |
11 |
|
fvprc |
⊢ ( ¬ 𝑈 ∈ V → ( 1st ‘ 𝑈 ) = ∅ ) |
12 |
11
|
fveq2d |
⊢ ( ¬ 𝑈 ∈ V → ( 1st ‘ ( 1st ‘ 𝑈 ) ) = ( 1st ‘ ∅ ) ) |
13 |
|
1st0 |
⊢ ( 1st ‘ ∅ ) = ∅ |
14 |
12 13
|
eqtr2di |
⊢ ( ¬ 𝑈 ∈ V → ∅ = ( 1st ‘ ( 1st ‘ 𝑈 ) ) ) |
15 |
10 14
|
eqtrd |
⊢ ( ¬ 𝑈 ∈ V → ( +𝑣 ‘ 𝑈 ) = ( 1st ‘ ( 1st ‘ 𝑈 ) ) ) |
16 |
9 15
|
pm2.61i |
⊢ ( +𝑣 ‘ 𝑈 ) = ( 1st ‘ ( 1st ‘ 𝑈 ) ) |
17 |
1 16
|
eqtri |
⊢ 𝐺 = ( 1st ‘ ( 1st ‘ 𝑈 ) ) |