Step |
Hyp |
Ref |
Expression |
1 |
|
efgmval.m |
⊢ 𝑀 = ( 𝑦 ∈ 𝐼 , 𝑧 ∈ 2o ↦ 〈 𝑦 , ( 1o ∖ 𝑧 ) 〉 ) |
2 |
|
elxp2 |
⊢ ( 𝐴 ∈ ( 𝐼 × 2o ) ↔ ∃ 𝑎 ∈ 𝐼 ∃ 𝑏 ∈ 2o 𝐴 = 〈 𝑎 , 𝑏 〉 ) |
3 |
1
|
efgmval |
⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 𝑎 𝑀 𝑏 ) = 〈 𝑎 , ( 1o ∖ 𝑏 ) 〉 ) |
4 |
3
|
fveq2d |
⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑀 ‘ 〈 𝑎 , ( 1o ∖ 𝑏 ) 〉 ) ) |
5 |
|
df-ov |
⊢ ( 𝑎 𝑀 ( 1o ∖ 𝑏 ) ) = ( 𝑀 ‘ 〈 𝑎 , ( 1o ∖ 𝑏 ) 〉 ) |
6 |
4 5
|
eqtr4di |
⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) = ( 𝑎 𝑀 ( 1o ∖ 𝑏 ) ) ) |
7 |
|
2oconcl |
⊢ ( 𝑏 ∈ 2o → ( 1o ∖ 𝑏 ) ∈ 2o ) |
8 |
1
|
efgmval |
⊢ ( ( 𝑎 ∈ 𝐼 ∧ ( 1o ∖ 𝑏 ) ∈ 2o ) → ( 𝑎 𝑀 ( 1o ∖ 𝑏 ) ) = 〈 𝑎 , ( 1o ∖ ( 1o ∖ 𝑏 ) ) 〉 ) |
9 |
7 8
|
sylan2 |
⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 𝑎 𝑀 ( 1o ∖ 𝑏 ) ) = 〈 𝑎 , ( 1o ∖ ( 1o ∖ 𝑏 ) ) 〉 ) |
10 |
|
1on |
⊢ 1o ∈ On |
11 |
10
|
onordi |
⊢ Ord 1o |
12 |
|
ordtr |
⊢ ( Ord 1o → Tr 1o ) |
13 |
|
trsucss |
⊢ ( Tr 1o → ( 𝑏 ∈ suc 1o → 𝑏 ⊆ 1o ) ) |
14 |
11 12 13
|
mp2b |
⊢ ( 𝑏 ∈ suc 1o → 𝑏 ⊆ 1o ) |
15 |
|
df-2o |
⊢ 2o = suc 1o |
16 |
14 15
|
eleq2s |
⊢ ( 𝑏 ∈ 2o → 𝑏 ⊆ 1o ) |
17 |
16
|
adantl |
⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → 𝑏 ⊆ 1o ) |
18 |
|
dfss4 |
⊢ ( 𝑏 ⊆ 1o ↔ ( 1o ∖ ( 1o ∖ 𝑏 ) ) = 𝑏 ) |
19 |
17 18
|
sylib |
⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 1o ∖ ( 1o ∖ 𝑏 ) ) = 𝑏 ) |
20 |
19
|
opeq2d |
⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → 〈 𝑎 , ( 1o ∖ ( 1o ∖ 𝑏 ) ) 〉 = 〈 𝑎 , 𝑏 〉 ) |
21 |
6 9 20
|
3eqtrd |
⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) = 〈 𝑎 , 𝑏 〉 ) |
22 |
|
fveq2 |
⊢ ( 𝐴 = 〈 𝑎 , 𝑏 〉 → ( 𝑀 ‘ 𝐴 ) = ( 𝑀 ‘ 〈 𝑎 , 𝑏 〉 ) ) |
23 |
|
df-ov |
⊢ ( 𝑎 𝑀 𝑏 ) = ( 𝑀 ‘ 〈 𝑎 , 𝑏 〉 ) |
24 |
22 23
|
eqtr4di |
⊢ ( 𝐴 = 〈 𝑎 , 𝑏 〉 → ( 𝑀 ‘ 𝐴 ) = ( 𝑎 𝑀 𝑏 ) ) |
25 |
24
|
fveq2d |
⊢ ( 𝐴 = 〈 𝑎 , 𝑏 〉 → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) ) |
26 |
|
id |
⊢ ( 𝐴 = 〈 𝑎 , 𝑏 〉 → 𝐴 = 〈 𝑎 , 𝑏 〉 ) |
27 |
25 26
|
eqeq12d |
⊢ ( 𝐴 = 〈 𝑎 , 𝑏 〉 → ( ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ↔ ( 𝑀 ‘ ( 𝑎 𝑀 𝑏 ) ) = 〈 𝑎 , 𝑏 〉 ) ) |
28 |
21 27
|
syl5ibrcom |
⊢ ( ( 𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o ) → ( 𝐴 = 〈 𝑎 , 𝑏 〉 → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) ) |
29 |
28
|
rexlimivv |
⊢ ( ∃ 𝑎 ∈ 𝐼 ∃ 𝑏 ∈ 2o 𝐴 = 〈 𝑎 , 𝑏 〉 → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) |
30 |
2 29
|
sylbi |
⊢ ( 𝐴 ∈ ( 𝐼 × 2o ) → ( 𝑀 ‘ ( 𝑀 ‘ 𝐴 ) ) = 𝐴 ) |