Step | Hyp | Ref
| Expression |
1 | | elxp2 5661 |
. 2
⊢ (𝐴 ∈ (𝐼 × 2o) ↔ ∃𝑎 ∈ 𝐼 ∃𝑏 ∈ 2o 𝐴 = ⟨𝑎, 𝑏⟩) |
2 | | efgmval.m |
. . . . . . . 8
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩) |
3 | 2 | efgmval 19502 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → (𝑎𝑀𝑏) = ⟨𝑎, (1o ∖ 𝑏)⟩) |
4 | 3 | fveq2d 6850 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → (𝑀‘(𝑎𝑀𝑏)) = (𝑀‘⟨𝑎, (1o ∖ 𝑏)⟩)) |
5 | | df-ov 7364 |
. . . . . 6
⊢ (𝑎𝑀(1o ∖ 𝑏)) = (𝑀‘⟨𝑎, (1o ∖ 𝑏)⟩) |
6 | 4, 5 | eqtr4di 2791 |
. . . . 5
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → (𝑀‘(𝑎𝑀𝑏)) = (𝑎𝑀(1o ∖ 𝑏))) |
7 | | 2oconcl 8453 |
. . . . . 6
⊢ (𝑏 ∈ 2o →
(1o ∖ 𝑏)
∈ 2o) |
8 | 2 | efgmval 19502 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐼 ∧ (1o ∖ 𝑏) ∈ 2o) →
(𝑎𝑀(1o ∖ 𝑏)) = ⟨𝑎, (1o ∖ (1o
∖ 𝑏))⟩) |
9 | 7, 8 | sylan2 594 |
. . . . 5
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → (𝑎𝑀(1o ∖ 𝑏)) = ⟨𝑎, (1o ∖ (1o
∖ 𝑏))⟩) |
10 | | 1on 8428 |
. . . . . . . . . . 11
⊢
1o ∈ On |
11 | 10 | onordi 6432 |
. . . . . . . . . 10
⊢ Ord
1o |
12 | | ordtr 6335 |
. . . . . . . . . 10
⊢ (Ord
1o → Tr 1o) |
13 | | trsucss 6409 |
. . . . . . . . . 10
⊢ (Tr
1o → (𝑏
∈ suc 1o → 𝑏 ⊆ 1o)) |
14 | 11, 12, 13 | mp2b 10 |
. . . . . . . . 9
⊢ (𝑏 ∈ suc 1o →
𝑏 ⊆
1o) |
15 | | df-2o 8417 |
. . . . . . . . 9
⊢
2o = suc 1o |
16 | 14, 15 | eleq2s 2852 |
. . . . . . . 8
⊢ (𝑏 ∈ 2o →
𝑏 ⊆
1o) |
17 | 16 | adantl 483 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → 𝑏 ⊆
1o) |
18 | | dfss4 4222 |
. . . . . . 7
⊢ (𝑏 ⊆ 1o ↔
(1o ∖ (1o ∖ 𝑏)) = 𝑏) |
19 | 17, 18 | sylib 217 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → (1o
∖ (1o ∖ 𝑏)) = 𝑏) |
20 | 19 | opeq2d 4841 |
. . . . 5
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → ⟨𝑎, (1o ∖
(1o ∖ 𝑏))⟩ = ⟨𝑎, 𝑏⟩) |
21 | 6, 9, 20 | 3eqtrd 2777 |
. . . 4
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → (𝑀‘(𝑎𝑀𝑏)) = ⟨𝑎, 𝑏⟩) |
22 | | fveq2 6846 |
. . . . . . 7
⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑀‘𝐴) = (𝑀‘⟨𝑎, 𝑏⟩)) |
23 | | df-ov 7364 |
. . . . . . 7
⊢ (𝑎𝑀𝑏) = (𝑀‘⟨𝑎, 𝑏⟩) |
24 | 22, 23 | eqtr4di 2791 |
. . . . . 6
⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑀‘𝐴) = (𝑎𝑀𝑏)) |
25 | 24 | fveq2d 6850 |
. . . . 5
⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑀‘(𝑀‘𝐴)) = (𝑀‘(𝑎𝑀𝑏))) |
26 | | id 22 |
. . . . 5
⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → 𝐴 = ⟨𝑎, 𝑏⟩) |
27 | 25, 26 | eqeq12d 2749 |
. . . 4
⊢ (𝐴 = ⟨𝑎, 𝑏⟩ → ((𝑀‘(𝑀‘𝐴)) = 𝐴 ↔ (𝑀‘(𝑎𝑀𝑏)) = ⟨𝑎, 𝑏⟩)) |
28 | 21, 27 | syl5ibrcom 247 |
. . 3
⊢ ((𝑎 ∈ 𝐼 ∧ 𝑏 ∈ 2o) → (𝐴 = ⟨𝑎, 𝑏⟩ → (𝑀‘(𝑀‘𝐴)) = 𝐴)) |
29 | 28 | rexlimivv 3193 |
. 2
⊢
(∃𝑎 ∈
𝐼 ∃𝑏 ∈ 2o 𝐴 = ⟨𝑎, 𝑏⟩ → (𝑀‘(𝑀‘𝐴)) = 𝐴) |
30 | 1, 29 | sylbi 216 |
1
⊢ (𝐴 ∈ (𝐼 × 2o) → (𝑀‘(𝑀‘𝐴)) = 𝐴) |