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