Step |
Hyp |
Ref |
Expression |
1 |
|
eleq1 |
⊢ ( 𝑔 = 𝐺 → ( 𝑔 ∈ ( V × V ) ↔ 𝐺 ∈ ( V × V ) ) ) |
2 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( 2nd ‘ 𝑔 ) = ( 2nd ‘ 𝐺 ) ) |
3 |
|
fveq2 |
⊢ ( 𝑔 = 𝐺 → ( .ef ‘ 𝑔 ) = ( .ef ‘ 𝐺 ) ) |
4 |
1 2 3
|
ifbieq12d |
⊢ ( 𝑔 = 𝐺 → if ( 𝑔 ∈ ( V × V ) , ( 2nd ‘ 𝑔 ) , ( .ef ‘ 𝑔 ) ) = if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) ) |
5 |
|
df-iedg |
⊢ iEdg = ( 𝑔 ∈ V ↦ if ( 𝑔 ∈ ( V × V ) , ( 2nd ‘ 𝑔 ) , ( .ef ‘ 𝑔 ) ) ) |
6 |
|
fvex |
⊢ ( 2nd ‘ 𝐺 ) ∈ V |
7 |
|
fvex |
⊢ ( .ef ‘ 𝐺 ) ∈ V |
8 |
6 7
|
ifex |
⊢ if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) ∈ V |
9 |
4 5 8
|
fvmpt |
⊢ ( 𝐺 ∈ V → ( iEdg ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) ) |
10 |
|
fvprc |
⊢ ( ¬ 𝐺 ∈ V → ( .ef ‘ 𝐺 ) = ∅ ) |
11 |
|
prcnel |
⊢ ( ¬ 𝐺 ∈ V → ¬ 𝐺 ∈ ( V × V ) ) |
12 |
11
|
iffalsed |
⊢ ( ¬ 𝐺 ∈ V → if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) = ( .ef ‘ 𝐺 ) ) |
13 |
|
fvprc |
⊢ ( ¬ 𝐺 ∈ V → ( iEdg ‘ 𝐺 ) = ∅ ) |
14 |
10 12 13
|
3eqtr4rd |
⊢ ( ¬ 𝐺 ∈ V → ( iEdg ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) ) |
15 |
9 14
|
pm2.61i |
⊢ ( iEdg ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 2nd ‘ 𝐺 ) , ( .ef ‘ 𝐺 ) ) |