Step | Hyp | Ref
| Expression |
1 | | elxp2 5056 |
. 2
⊢ (𝐴 ∈ (𝐼 × 2𝑜) ↔
∃𝑎 ∈ 𝐼 ∃𝑏 ∈ 2𝑜 𝐴 = 〈𝑎, 𝑏〉) |
2 | | efgmval.m |
. . . . . . . 8
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
3 | 2 | efgmval 17948 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) → (𝑎𝑀𝑏) = 〈𝑎, (1𝑜 ∖ 𝑏)〉) |
4 | 3 | fveq2d 6107 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) → (𝑀‘(𝑎𝑀𝑏)) = (𝑀‘〈𝑎, (1𝑜 ∖ 𝑏)〉)) |
5 | | df-ov 6552 |
. . . . . 6
⊢ (𝑎𝑀(1𝑜 ∖ 𝑏)) = (𝑀‘〈𝑎, (1𝑜 ∖ 𝑏)〉) |
6 | 4, 5 | syl6eqr 2662 |
. . . . 5
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) → (𝑀‘(𝑎𝑀𝑏)) = (𝑎𝑀(1𝑜 ∖ 𝑏))) |
7 | | 2oconcl 7470 |
. . . . . 6
⊢ (𝑏 ∈ 2𝑜
→ (1𝑜 ∖ 𝑏) ∈
2𝑜) |
8 | 2 | efgmval 17948 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐼 ∧ (1𝑜 ∖ 𝑏) ∈ 2𝑜)
→ (𝑎𝑀(1𝑜 ∖ 𝑏)) = 〈𝑎, (1𝑜 ∖
(1𝑜 ∖ 𝑏))〉) |
9 | 7, 8 | sylan2 490 |
. . . . 5
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) → (𝑎𝑀(1𝑜 ∖ 𝑏)) = 〈𝑎, (1𝑜 ∖
(1𝑜 ∖ 𝑏))〉) |
10 | | 1on 7454 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ On |
11 | 10 | onordi 5749 |
. . . . . . . . . 10
⊢ Ord
1𝑜 |
12 | | ordtr 5654 |
. . . . . . . . . 10
⊢ (Ord
1𝑜 → Tr 1𝑜) |
13 | | trsucss 5728 |
. . . . . . . . . 10
⊢ (Tr
1𝑜 → (𝑏 ∈ suc 1𝑜 →
𝑏 ⊆
1𝑜)) |
14 | 11, 12, 13 | mp2b 10 |
. . . . . . . . 9
⊢ (𝑏 ∈ suc
1𝑜 → 𝑏 ⊆
1𝑜) |
15 | | df-2o 7448 |
. . . . . . . . 9
⊢
2𝑜 = suc 1𝑜 |
16 | 14, 15 | eleq2s 2706 |
. . . . . . . 8
⊢ (𝑏 ∈ 2𝑜
→ 𝑏 ⊆
1𝑜) |
17 | 16 | adantl 481 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) → 𝑏 ⊆
1𝑜) |
18 | | dfss4 3820 |
. . . . . . 7
⊢ (𝑏 ⊆ 1𝑜
↔ (1𝑜 ∖ (1𝑜 ∖ 𝑏)) = 𝑏) |
19 | 17, 18 | sylib 207 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) →
(1𝑜 ∖ (1𝑜 ∖ 𝑏)) = 𝑏) |
20 | 19 | opeq2d 4347 |
. . . . 5
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) →
〈𝑎,
(1𝑜 ∖ (1𝑜 ∖ 𝑏))〉 = 〈𝑎, 𝑏〉) |
21 | 6, 9, 20 | 3eqtrd 2648 |
. . . 4
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) → (𝑀‘(𝑎𝑀𝑏)) = 〈𝑎, 𝑏〉) |
22 | | fveq2 6103 |
. . . . . . 7
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑀‘𝐴) = (𝑀‘〈𝑎, 𝑏〉)) |
23 | | df-ov 6552 |
. . . . . . 7
⊢ (𝑎𝑀𝑏) = (𝑀‘〈𝑎, 𝑏〉) |
24 | 22, 23 | syl6eqr 2662 |
. . . . . 6
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑀‘𝐴) = (𝑎𝑀𝑏)) |
25 | 24 | fveq2d 6107 |
. . . . 5
⊢ (𝐴 = 〈𝑎, 𝑏〉 → (𝑀‘(𝑀‘𝐴)) = (𝑀‘(𝑎𝑀𝑏))) |
26 | | id 22 |
. . . . 5
⊢ (𝐴 = 〈𝑎, 𝑏〉 → 𝐴 = 〈𝑎, 𝑏〉) |
27 | 25, 26 | eqeq12d 2625 |
. . . 4
⊢ (𝐴 = 〈𝑎, 𝑏〉 → ((𝑀‘(𝑀‘𝐴)) = 𝐴 ↔ (𝑀‘(𝑎𝑀𝑏)) = 〈𝑎, 𝑏〉)) |
28 | 21, 27 | syl5ibrcom 236 |
. . 3
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2𝑜) → (𝐴 = 〈𝑎, 𝑏〉 → (𝑀‘(𝑀‘𝐴)) = 𝐴)) |
29 | 28 | rexlimivv 3018 |
. 2
⊢
(∃𝑎 ∈
𝐼 ∃𝑏 ∈ 2𝑜 𝐴 = 〈𝑎, 𝑏〉 → (𝑀‘(𝑀‘𝐴)) = 𝐴) |
30 | 1, 29 | sylbi 206 |
1
⊢ (𝐴 ∈ (𝐼 × 2𝑜) →
(𝑀‘(𝑀‘𝐴)) = 𝐴) |