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 ‘ 𝐸 ) ∈ 𝑈 )