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