Step | Hyp | Ref
| Expression |
1 | | eqidd 2178 |
. . 3
⊢ (𝑅 ∈ SRing →
(Base‘𝑅) =
(Base‘𝑅)) |
2 | | eqidd 2178 |
. . 3
⊢ (𝑅 ∈ SRing →
(∥r‘𝑅) = (∥r‘𝑅)) |
3 | | id 19 |
. . 3
⊢ (𝑅 ∈ SRing → 𝑅 ∈ SRing) |
4 | | eqidd 2178 |
. . 3
⊢ (𝑅 ∈ SRing →
(.r‘𝑅) =
(.r‘𝑅)) |
5 | 1, 2, 3, 4 | dvdsrvald 13260 |
. 2
⊢ (𝑅 ∈ SRing →
(∥r‘𝑅) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦)}) |
6 | | basfn 12519 |
. . . . 5
⊢ Base Fn
V |
7 | | elex 2748 |
. . . . 5
⊢ (𝑅 ∈ SRing → 𝑅 ∈ V) |
8 | | funfvex 5532 |
. . . . . 6
⊢ ((Fun
Base ∧ 𝑅 ∈ dom
Base) → (Base‘𝑅)
∈ V) |
9 | 8 | funfni 5316 |
. . . . 5
⊢ ((Base Fn
V ∧ 𝑅 ∈ V) →
(Base‘𝑅) ∈
V) |
10 | 6, 7, 9 | sylancr 414 |
. . . 4
⊢ (𝑅 ∈ SRing →
(Base‘𝑅) ∈
V) |
11 | | xpexg 4740 |
. . . 4
⊢
(((Base‘𝑅)
∈ V ∧ (Base‘𝑅) ∈ V) → ((Base‘𝑅) × (Base‘𝑅)) ∈ V) |
12 | 10, 10, 11 | syl2anc 411 |
. . 3
⊢ (𝑅 ∈ SRing →
((Base‘𝑅) ×
(Base‘𝑅)) ∈
V) |
13 | | simprr 531 |
. . . . . . . 8
⊢ (((𝑅 ∈ SRing ∧ 𝑥 ∈ (Base‘𝑅)) ∧ (𝑧 ∈ (Base‘𝑅) ∧ (𝑧(.r‘𝑅)𝑥) = 𝑦)) → (𝑧(.r‘𝑅)𝑥) = 𝑦) |
14 | | simpll 527 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SRing ∧ 𝑥 ∈ (Base‘𝑅)) ∧ (𝑧 ∈ (Base‘𝑅) ∧ (𝑧(.r‘𝑅)𝑥) = 𝑦)) → 𝑅 ∈ SRing) |
15 | | simprl 529 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SRing ∧ 𝑥 ∈ (Base‘𝑅)) ∧ (𝑧 ∈ (Base‘𝑅) ∧ (𝑧(.r‘𝑅)𝑥) = 𝑦)) → 𝑧 ∈ (Base‘𝑅)) |
16 | | simplr 528 |
. . . . . . . . 9
⊢ (((𝑅 ∈ SRing ∧ 𝑥 ∈ (Base‘𝑅)) ∧ (𝑧 ∈ (Base‘𝑅) ∧ (𝑧(.r‘𝑅)𝑥) = 𝑦)) → 𝑥 ∈ (Base‘𝑅)) |
17 | | eqid 2177 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
18 | | eqid 2177 |
. . . . . . . . . 10
⊢
(.r‘𝑅) = (.r‘𝑅) |
19 | 17, 18 | srgcl 13151 |
. . . . . . . . 9
⊢ ((𝑅 ∈ SRing ∧ 𝑧 ∈ (Base‘𝑅) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑧(.r‘𝑅)𝑥) ∈ (Base‘𝑅)) |
20 | 14, 15, 16, 19 | syl3anc 1238 |
. . . . . . . 8
⊢ (((𝑅 ∈ SRing ∧ 𝑥 ∈ (Base‘𝑅)) ∧ (𝑧 ∈ (Base‘𝑅) ∧ (𝑧(.r‘𝑅)𝑥) = 𝑦)) → (𝑧(.r‘𝑅)𝑥) ∈ (Base‘𝑅)) |
21 | 13, 20 | eqeltrrd 2255 |
. . . . . . 7
⊢ (((𝑅 ∈ SRing ∧ 𝑥 ∈ (Base‘𝑅)) ∧ (𝑧 ∈ (Base‘𝑅) ∧ (𝑧(.r‘𝑅)𝑥) = 𝑦)) → 𝑦 ∈ (Base‘𝑅)) |
22 | 21 | rexlimdvaa 2595 |
. . . . . 6
⊢ ((𝑅 ∈ SRing ∧ 𝑥 ∈ (Base‘𝑅)) → (∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦 → 𝑦 ∈ (Base‘𝑅))) |
23 | 22 | imdistanda 448 |
. . . . 5
⊢ (𝑅 ∈ SRing → ((𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦) → (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅)))) |
24 | 23 | ssopab2dv 4278 |
. . . 4
⊢ (𝑅 ∈ SRing →
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))}) |
25 | | df-xp 4632 |
. . . 4
⊢
((Base‘𝑅)
× (Base‘𝑅)) =
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑅) ∧ 𝑦 ∈ (Base‘𝑅))} |
26 | 24, 25 | sseqtrrdi 3204 |
. . 3
⊢ (𝑅 ∈ SRing →
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦)} ⊆ ((Base‘𝑅) × (Base‘𝑅))) |
27 | 12, 26 | ssexd 4143 |
. 2
⊢ (𝑅 ∈ SRing →
{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (Base‘𝑅) ∧ ∃𝑧 ∈ (Base‘𝑅)(𝑧(.r‘𝑅)𝑥) = 𝑦)} ∈ V) |
28 | 5, 27 | eqeltrd 2254 |
1
⊢ (𝑅 ∈ SRing →
(∥r‘𝑅) ∈ V) |