| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | n0i 4339 | . 2
⊢ (𝑋 ∈ 𝑄 → ¬ 𝑄 = ∅) | 
| 2 |  | pf1rcl.q | . . . 4
⊢ 𝑄 = ran
(eval1‘𝑅) | 
| 3 |  | eqid 2736 | . . . . . 6
⊢
(eval1‘𝑅) = (eval1‘𝑅) | 
| 4 |  | eqid 2736 | . . . . . 6
⊢
(1o eval 𝑅) = (1o eval 𝑅) | 
| 5 |  | eqid 2736 | . . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 6 | 3, 4, 5 | evl1fval 22333 | . . . . 5
⊢
(eval1‘𝑅) = ((𝑥 ∈ ((Base‘𝑅) ↑m ((Base‘𝑅) ↑m
1o)) ↦ (𝑥
∘ (𝑦 ∈
(Base‘𝑅) ↦
(1o × {𝑦})))) ∘ (1o eval 𝑅)) | 
| 7 | 6 | rneqi 5947 | . . . 4
⊢ ran
(eval1‘𝑅)
= ran ((𝑥 ∈
((Base‘𝑅)
↑m ((Base‘𝑅) ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1o ×
{𝑦})))) ∘
(1o eval 𝑅)) | 
| 8 |  | rnco2 6272 | . . . 4
⊢ ran
((𝑥 ∈
((Base‘𝑅)
↑m ((Base‘𝑅) ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1o ×
{𝑦})))) ∘
(1o eval 𝑅)) =
((𝑥 ∈
((Base‘𝑅)
↑m ((Base‘𝑅) ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1o ×
{𝑦})))) “ ran
(1o eval 𝑅)) | 
| 9 | 2, 7, 8 | 3eqtri 2768 | . . 3
⊢ 𝑄 = ((𝑥 ∈ ((Base‘𝑅) ↑m ((Base‘𝑅) ↑m
1o)) ↦ (𝑥
∘ (𝑦 ∈
(Base‘𝑅) ↦
(1o × {𝑦})))) “ ran (1o eval 𝑅)) | 
| 10 |  | inss2 4237 | . . . . 5
⊢ (dom
(𝑥 ∈
((Base‘𝑅)
↑m ((Base‘𝑅) ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1o ×
{𝑦})))) ∩ ran
(1o eval 𝑅))
⊆ ran (1o eval 𝑅) | 
| 11 |  | neq0 4351 | . . . . . . 7
⊢ (¬
ran (1o eval 𝑅)
= ∅ ↔ ∃𝑥
𝑥 ∈ ran (1o
eval 𝑅)) | 
| 12 | 4, 5 | evlval 22120 | . . . . . . . . . . 11
⊢
(1o eval 𝑅) = ((1o evalSub 𝑅)‘(Base‘𝑅)) | 
| 13 | 12 | rneqi 5947 | . . . . . . . . . 10
⊢ ran
(1o eval 𝑅) =
ran ((1o evalSub 𝑅)‘(Base‘𝑅)) | 
| 14 | 13 | mpfrcl 22110 | . . . . . . . . 9
⊢ (𝑥 ∈ ran (1o eval
𝑅) → (1o
∈ V ∧ 𝑅 ∈
CRing ∧ (Base‘𝑅)
∈ (SubRing‘𝑅))) | 
| 15 | 14 | simp2d 1143 | . . . . . . . 8
⊢ (𝑥 ∈ ran (1o eval
𝑅) → 𝑅 ∈ CRing) | 
| 16 | 15 | exlimiv 1929 | . . . . . . 7
⊢
(∃𝑥 𝑥 ∈ ran (1o eval
𝑅) → 𝑅 ∈ CRing) | 
| 17 | 11, 16 | sylbi 217 | . . . . . 6
⊢ (¬
ran (1o eval 𝑅)
= ∅ → 𝑅 ∈
CRing) | 
| 18 | 17 | con1i 147 | . . . . 5
⊢ (¬
𝑅 ∈ CRing → ran
(1o eval 𝑅) =
∅) | 
| 19 |  | sseq0 4402 | . . . . 5
⊢ (((dom
(𝑥 ∈
((Base‘𝑅)
↑m ((Base‘𝑅) ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1o ×
{𝑦})))) ∩ ran
(1o eval 𝑅))
⊆ ran (1o eval 𝑅) ∧ ran (1o eval 𝑅) = ∅) → (dom (𝑥 ∈ ((Base‘𝑅) ↑m
((Base‘𝑅)
↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1o × {𝑦})))) ∩ ran (1o
eval 𝑅)) =
∅) | 
| 20 | 10, 18, 19 | sylancr 587 | . . . 4
⊢ (¬
𝑅 ∈ CRing → (dom
(𝑥 ∈
((Base‘𝑅)
↑m ((Base‘𝑅) ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1o ×
{𝑦})))) ∩ ran
(1o eval 𝑅)) =
∅) | 
| 21 |  | imadisj 6097 | . . . 4
⊢ (((𝑥 ∈ ((Base‘𝑅) ↑m
((Base‘𝑅)
↑m 1o)) ↦ (𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1o × {𝑦})))) “ ran (1o
eval 𝑅)) = ∅ ↔
(dom (𝑥 ∈
((Base‘𝑅)
↑m ((Base‘𝑅) ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1o ×
{𝑦})))) ∩ ran
(1o eval 𝑅)) =
∅) | 
| 22 | 20, 21 | sylibr 234 | . . 3
⊢ (¬
𝑅 ∈ CRing →
((𝑥 ∈
((Base‘𝑅)
↑m ((Base‘𝑅) ↑m 1o)) ↦
(𝑥 ∘ (𝑦 ∈ (Base‘𝑅) ↦ (1o ×
{𝑦})))) “ ran
(1o eval 𝑅)) =
∅) | 
| 23 | 9, 22 | eqtrid 2788 | . 2
⊢ (¬
𝑅 ∈ CRing → 𝑄 = ∅) | 
| 24 | 1, 23 | nsyl2 141 | 1
⊢ (𝑋 ∈ 𝑄 → 𝑅 ∈ CRing) |