Step |
Hyp |
Ref |
Expression |
1 |
|
fvex |
⊢ ( 𝐺 ‘ ∅ ) ∈ V |
2 |
|
fvex |
⊢ ( 𝐺 ‘ 1o ) ∈ V |
3 |
|
fnpr2o |
⊢ ( ( ( 𝐺 ‘ ∅ ) ∈ V ∧ ( 𝐺 ‘ 1o ) ∈ V ) → { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } Fn 2o ) |
4 |
1 2 3
|
mp2an |
⊢ { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } Fn 2o |
5 |
4
|
a1i |
⊢ ( 𝐺 Fn 2o → { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } Fn 2o ) |
6 |
|
id |
⊢ ( 𝐺 Fn 2o → 𝐺 Fn 2o ) |
7 |
|
elpri |
⊢ ( 𝑘 ∈ { ∅ , 1o } → ( 𝑘 = ∅ ∨ 𝑘 = 1o ) ) |
8 |
|
df2o3 |
⊢ 2o = { ∅ , 1o } |
9 |
7 8
|
eleq2s |
⊢ ( 𝑘 ∈ 2o → ( 𝑘 = ∅ ∨ 𝑘 = 1o ) ) |
10 |
|
fvpr0o |
⊢ ( ( 𝐺 ‘ ∅ ) ∈ V → ( { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } ‘ ∅ ) = ( 𝐺 ‘ ∅ ) ) |
11 |
1 10
|
ax-mp |
⊢ ( { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } ‘ ∅ ) = ( 𝐺 ‘ ∅ ) |
12 |
|
fveq2 |
⊢ ( 𝑘 = ∅ → ( { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } ‘ 𝑘 ) = ( { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } ‘ ∅ ) ) |
13 |
|
fveq2 |
⊢ ( 𝑘 = ∅ → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ ∅ ) ) |
14 |
11 12 13
|
3eqtr4a |
⊢ ( 𝑘 = ∅ → ( { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) |
15 |
|
fvpr1o |
⊢ ( ( 𝐺 ‘ 1o ) ∈ V → ( { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } ‘ 1o ) = ( 𝐺 ‘ 1o ) ) |
16 |
2 15
|
ax-mp |
⊢ ( { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } ‘ 1o ) = ( 𝐺 ‘ 1o ) |
17 |
|
fveq2 |
⊢ ( 𝑘 = 1o → ( { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } ‘ 𝑘 ) = ( { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } ‘ 1o ) ) |
18 |
|
fveq2 |
⊢ ( 𝑘 = 1o → ( 𝐺 ‘ 𝑘 ) = ( 𝐺 ‘ 1o ) ) |
19 |
16 17 18
|
3eqtr4a |
⊢ ( 𝑘 = 1o → ( { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) |
20 |
14 19
|
jaoi |
⊢ ( ( 𝑘 = ∅ ∨ 𝑘 = 1o ) → ( { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) |
21 |
9 20
|
syl |
⊢ ( 𝑘 ∈ 2o → ( { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) |
22 |
21
|
adantl |
⊢ ( ( 𝐺 Fn 2o ∧ 𝑘 ∈ 2o ) → ( { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } ‘ 𝑘 ) = ( 𝐺 ‘ 𝑘 ) ) |
23 |
5 6 22
|
eqfnfvd |
⊢ ( 𝐺 Fn 2o → { 〈 ∅ , ( 𝐺 ‘ ∅ ) 〉 , 〈 1o , ( 𝐺 ‘ 1o ) 〉 } = 𝐺 ) |