Metamath Proof Explorer


Theorem estrcbasbas

Description: An element of the base set of the base set of the category of extensible structures (i.e. the base set of an extensible structure) belongs to the considered weak universe. (Contributed by AV, 22-Mar-2020)

Ref Expression
Hypotheses estrcbasbas.c 𝐶 = ( ExtStrCat ‘ 𝑈 )
estrcbasbas.b 𝐵 = ( Base ‘ 𝐶 )
estrcbasbas.u ( 𝜑𝑈 ∈ WUni )
Assertion estrcbasbas ( ( 𝜑𝐸𝐵 ) → ( Base ‘ 𝐸 ) ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 estrcbasbas.c 𝐶 = ( ExtStrCat ‘ 𝑈 )
2 estrcbasbas.b 𝐵 = ( Base ‘ 𝐶 )
3 estrcbasbas.u ( 𝜑𝑈 ∈ WUni )
4 1 3 estrcbas ( 𝜑𝑈 = ( Base ‘ 𝐶 ) )
5 2 4 eqtr4id ( 𝜑𝐵 = 𝑈 )
6 5 eleq2d ( 𝜑 → ( 𝐸𝐵𝐸𝑈 ) )
7 baseid Base = Slot ( Base ‘ ndx )
8 simpl ( ( 𝑈 ∈ WUni ∧ 𝐸𝑈 ) → 𝑈 ∈ WUni )
9 simpr ( ( 𝑈 ∈ WUni ∧ 𝐸𝑈 ) → 𝐸𝑈 )
10 7 8 9 wunstr ( ( 𝑈 ∈ WUni ∧ 𝐸𝑈 ) → ( Base ‘ 𝐸 ) ∈ 𝑈 )
11 10 ex ( 𝑈 ∈ WUni → ( 𝐸𝑈 → ( Base ‘ 𝐸 ) ∈ 𝑈 ) )
12 3 11 syl ( 𝜑 → ( 𝐸𝑈 → ( Base ‘ 𝐸 ) ∈ 𝑈 ) )
13 6 12 sylbid ( 𝜑 → ( 𝐸𝐵 → ( Base ‘ 𝐸 ) ∈ 𝑈 ) )
14 13 imp ( ( 𝜑𝐸𝐵 ) → ( Base ‘ 𝐸 ) ∈ 𝑈 )