Step 
Hyp 
Ref 
Expression 
1 

pf1rcl.q 
⊢ 𝑄 = ran ( eval_{1} ‘ 𝑅 ) 
2 

n0i 
⊢ ( 𝑋 ∈ 𝑄 → ¬ 𝑄 = ∅ ) 
3 

eqid 
⊢ ( eval_{1} ‘ 𝑅 ) = ( eval_{1} ‘ 𝑅 ) 
4 

eqid 
⊢ ( 1_{o} eval 𝑅 ) = ( 1_{o} eval 𝑅 ) 
5 

eqid 
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) 
6 
3 4 5

evl1fval 
⊢ ( eval_{1} ‘ 𝑅 ) = ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑_{m} ( ( Base ‘ 𝑅 ) ↑_{m} 1_{o} ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1_{o} × { 𝑦 } ) ) ) ) ∘ ( 1_{o} eval 𝑅 ) ) 
7 
6

rneqi 
⊢ ran ( eval_{1} ‘ 𝑅 ) = ran ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑_{m} ( ( Base ‘ 𝑅 ) ↑_{m} 1_{o} ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1_{o} × { 𝑦 } ) ) ) ) ∘ ( 1_{o} eval 𝑅 ) ) 
8 

rnco2 
⊢ ran ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑_{m} ( ( Base ‘ 𝑅 ) ↑_{m} 1_{o} ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1_{o} × { 𝑦 } ) ) ) ) ∘ ( 1_{o} eval 𝑅 ) ) = ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑_{m} ( ( Base ‘ 𝑅 ) ↑_{m} 1_{o} ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1_{o} × { 𝑦 } ) ) ) ) “ ran ( 1_{o} eval 𝑅 ) ) 
9 
1 7 8

3eqtri 
⊢ 𝑄 = ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑_{m} ( ( Base ‘ 𝑅 ) ↑_{m} 1_{o} ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1_{o} × { 𝑦 } ) ) ) ) “ ran ( 1_{o} eval 𝑅 ) ) 
10 

inss2 
⊢ ( dom ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑_{m} ( ( Base ‘ 𝑅 ) ↑_{m} 1_{o} ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1_{o} × { 𝑦 } ) ) ) ) ∩ ran ( 1_{o} eval 𝑅 ) ) ⊆ ran ( 1_{o} eval 𝑅 ) 
11 

neq0 
⊢ ( ¬ ran ( 1_{o} eval 𝑅 ) = ∅ ↔ ∃ 𝑥 𝑥 ∈ ran ( 1_{o} eval 𝑅 ) ) 
12 
4 5

evlval 
⊢ ( 1_{o} eval 𝑅 ) = ( ( 1_{o} evalSub 𝑅 ) ‘ ( Base ‘ 𝑅 ) ) 
13 
12

rneqi 
⊢ ran ( 1_{o} eval 𝑅 ) = ran ( ( 1_{o} evalSub 𝑅 ) ‘ ( Base ‘ 𝑅 ) ) 
14 
13

mpfrcl 
⊢ ( 𝑥 ∈ ran ( 1_{o} eval 𝑅 ) → ( 1_{o} ∈ V ∧ 𝑅 ∈ CRing ∧ ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) ) ) 
15 
14

simp2d 
⊢ ( 𝑥 ∈ ran ( 1_{o} eval 𝑅 ) → 𝑅 ∈ CRing ) 
16 
15

exlimiv 
⊢ ( ∃ 𝑥 𝑥 ∈ ran ( 1_{o} eval 𝑅 ) → 𝑅 ∈ CRing ) 
17 
11 16

sylbi 
⊢ ( ¬ ran ( 1_{o} eval 𝑅 ) = ∅ → 𝑅 ∈ CRing ) 
18 
17

con1i 
⊢ ( ¬ 𝑅 ∈ CRing → ran ( 1_{o} eval 𝑅 ) = ∅ ) 
19 

sseq0 
⊢ ( ( ( dom ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑_{m} ( ( Base ‘ 𝑅 ) ↑_{m} 1_{o} ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1_{o} × { 𝑦 } ) ) ) ) ∩ ran ( 1_{o} eval 𝑅 ) ) ⊆ ran ( 1_{o} eval 𝑅 ) ∧ ran ( 1_{o} eval 𝑅 ) = ∅ ) → ( dom ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑_{m} ( ( Base ‘ 𝑅 ) ↑_{m} 1_{o} ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1_{o} × { 𝑦 } ) ) ) ) ∩ ran ( 1_{o} eval 𝑅 ) ) = ∅ ) 
20 
10 18 19

sylancr 
⊢ ( ¬ 𝑅 ∈ CRing → ( dom ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑_{m} ( ( Base ‘ 𝑅 ) ↑_{m} 1_{o} ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1_{o} × { 𝑦 } ) ) ) ) ∩ ran ( 1_{o} eval 𝑅 ) ) = ∅ ) 
21 

imadisj 
⊢ ( ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑_{m} ( ( Base ‘ 𝑅 ) ↑_{m} 1_{o} ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1_{o} × { 𝑦 } ) ) ) ) “ ran ( 1_{o} eval 𝑅 ) ) = ∅ ↔ ( dom ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑_{m} ( ( Base ‘ 𝑅 ) ↑_{m} 1_{o} ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1_{o} × { 𝑦 } ) ) ) ) ∩ ran ( 1_{o} eval 𝑅 ) ) = ∅ ) 
22 
20 21

sylibr 
⊢ ( ¬ 𝑅 ∈ CRing → ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑_{m} ( ( Base ‘ 𝑅 ) ↑_{m} 1_{o} ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( 1_{o} × { 𝑦 } ) ) ) ) “ ran ( 1_{o} eval 𝑅 ) ) = ∅ ) 
23 
9 22

syl5eq 
⊢ ( ¬ 𝑅 ∈ CRing → 𝑄 = ∅ ) 
24 
2 23

nsyl2 
⊢ ( 𝑋 ∈ 𝑄 → 𝑅 ∈ CRing ) 