| Step | Hyp | Ref
| Expression |
| 1 | | r1fnon 9807 |
. . 3
⊢
𝑅1 Fn On |
| 2 | | dffn2 6738 |
. . 3
⊢
(𝑅1 Fn On ↔
𝑅1:On⟶V) |
| 3 | 1, 2 | mpbi 230 |
. 2
⊢
𝑅1:On⟶V |
| 4 | | eloni 6394 |
. . . . 5
⊢ (𝑥 ∈ On → Ord 𝑥) |
| 5 | | eloni 6394 |
. . . . 5
⊢ (𝑦 ∈ On → Ord 𝑦) |
| 6 | | ordtri3or 6416 |
. . . . 5
⊢ ((Ord
𝑥 ∧ Ord 𝑦) → (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) |
| 7 | 4, 5, 6 | syl2an 596 |
. . . 4
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) |
| 8 | | sdomirr 9154 |
. . . . . . . . 9
⊢ ¬
(𝑅1‘𝑦) ≺ (𝑅1‘𝑦) |
| 9 | | r1sdom 9814 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → (𝑅1‘𝑥) ≺
(𝑅1‘𝑦)) |
| 10 | | breq1 5146 |
. . . . . . . . . 10
⊢
((𝑅1‘𝑥) = (𝑅1‘𝑦) →
((𝑅1‘𝑥) ≺ (𝑅1‘𝑦) ↔
(𝑅1‘𝑦) ≺ (𝑅1‘𝑦))) |
| 11 | 9, 10 | syl5ibcom 245 |
. . . . . . . . 9
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → ((𝑅1‘𝑥) =
(𝑅1‘𝑦) → (𝑅1‘𝑦) ≺
(𝑅1‘𝑦))) |
| 12 | 8, 11 | mtoi 199 |
. . . . . . . 8
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → ¬
(𝑅1‘𝑥) = (𝑅1‘𝑦)) |
| 13 | 12 | 3adant1 1131 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → ¬
(𝑅1‘𝑥) = (𝑅1‘𝑦)) |
| 14 | 13 | pm2.21d 121 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑥 ∈ 𝑦) → ((𝑅1‘𝑥) =
(𝑅1‘𝑦) → 𝑥 = 𝑦)) |
| 15 | 14 | 3expia 1122 |
. . . . 5
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 ∈ 𝑦 → ((𝑅1‘𝑥) =
(𝑅1‘𝑦) → 𝑥 = 𝑦))) |
| 16 | | ax-1 6 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑅1‘𝑥) =
(𝑅1‘𝑦) → 𝑥 = 𝑦)) |
| 17 | 16 | a1i 11 |
. . . . 5
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑥 = 𝑦 → ((𝑅1‘𝑥) =
(𝑅1‘𝑦) → 𝑥 = 𝑦))) |
| 18 | | r1sdom 9814 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → (𝑅1‘𝑦) ≺
(𝑅1‘𝑥)) |
| 19 | | breq2 5147 |
. . . . . . . . . 10
⊢
((𝑅1‘𝑥) = (𝑅1‘𝑦) →
((𝑅1‘𝑦) ≺ (𝑅1‘𝑥) ↔
(𝑅1‘𝑦) ≺ (𝑅1‘𝑦))) |
| 20 | 18, 19 | syl5ibcom 245 |
. . . . . . . . 9
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ((𝑅1‘𝑥) =
(𝑅1‘𝑦) → (𝑅1‘𝑦) ≺
(𝑅1‘𝑦))) |
| 21 | 8, 20 | mtoi 199 |
. . . . . . . 8
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → ¬
(𝑅1‘𝑥) = (𝑅1‘𝑦)) |
| 22 | 21 | 3adant2 1132 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑦 ∈ 𝑥) → ¬
(𝑅1‘𝑥) = (𝑅1‘𝑦)) |
| 23 | 22 | pm2.21d 121 |
. . . . . 6
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On ∧ 𝑦 ∈ 𝑥) → ((𝑅1‘𝑥) =
(𝑅1‘𝑦) → 𝑥 = 𝑦)) |
| 24 | 23 | 3expia 1122 |
. . . . 5
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (𝑦 ∈ 𝑥 → ((𝑅1‘𝑥) =
(𝑅1‘𝑦) → 𝑥 = 𝑦))) |
| 25 | 15, 17, 24 | 3jaod 1431 |
. . . 4
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ((𝑅1‘𝑥) =
(𝑅1‘𝑦) → 𝑥 = 𝑦))) |
| 26 | 7, 25 | mpd 15 |
. . 3
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) →
((𝑅1‘𝑥) = (𝑅1‘𝑦) → 𝑥 = 𝑦)) |
| 27 | 26 | rgen2 3199 |
. 2
⊢
∀𝑥 ∈ On
∀𝑦 ∈ On
((𝑅1‘𝑥) = (𝑅1‘𝑦) → 𝑥 = 𝑦) |
| 28 | | dff13 7275 |
. 2
⊢
(𝑅1:On–1-1→V ↔ (𝑅1:On⟶V
∧ ∀𝑥 ∈ On
∀𝑦 ∈ On
((𝑅1‘𝑥) = (𝑅1‘𝑦) → 𝑥 = 𝑦))) |
| 29 | 3, 27, 28 | mpbir2an 711 |
1
⊢
𝑅1:On–1-1→V |