Description: Lemma 2 for funcringcsetcALTV2 . (Contributed by AV, 15-Feb-2020) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | funcringcsetcALTV2.r | ⊢ 𝑅 = ( RingCat ‘ 𝑈 ) | |
| funcringcsetcALTV2.s | ⊢ 𝑆 = ( SetCat ‘ 𝑈 ) | ||
| funcringcsetcALTV2.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | ||
| funcringcsetcALTV2.c | ⊢ 𝐶 = ( Base ‘ 𝑆 ) | ||
| funcringcsetcALTV2.u | ⊢ ( 𝜑 → 𝑈 ∈ WUni ) | ||
| funcringcsetcALTV2.f | ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) ) | ||
| Assertion | funcringcsetcALTV2lem2 | ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | funcringcsetcALTV2.r | ⊢ 𝑅 = ( RingCat ‘ 𝑈 ) | |
| 2 | funcringcsetcALTV2.s | ⊢ 𝑆 = ( SetCat ‘ 𝑈 ) | |
| 3 | funcringcsetcALTV2.b | ⊢ 𝐵 = ( Base ‘ 𝑅 ) | |
| 4 | funcringcsetcALTV2.c | ⊢ 𝐶 = ( Base ‘ 𝑆 ) | |
| 5 | funcringcsetcALTV2.u | ⊢ ( 𝜑 → 𝑈 ∈ WUni ) | |
| 6 | funcringcsetcALTV2.f | ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) ) | |
| 7 | 1 2 3 4 5 6 | funcringcsetcALTV2lem1 | ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) = ( Base ‘ 𝑋 ) ) |
| 8 | 1 3 5 | ringcbasbas | ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( Base ‘ 𝑋 ) ∈ 𝑈 ) |
| 9 | 7 8 | eqeltrd | ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 ) |