gruima

Description: A Grothendieck universe contains image sets drawn from its members. (Contributed by Mario Carneiro, 9-Jun-2013)

		Ref	Expression
	Assertion	gruima	$⊢ (U \in Univ \land Fun F \land F [A] \subseteq U) \to (A \in U \to F [A] \in U)$

Proof

Step	Hyp	Ref	Expression
1		simpl2	$⊢ ((U \in Univ \land Fun F \land F [A] \subseteq U) \land A \in U) \to Fun F$
2		funrel	$⊢ Fun F \to Rel F$
3		df-ima	$⊢ F [A] = ran ({F ↾}_{A})$
4		resres	$⊢ {({F ↾}_{dom F}) ↾}_{A} = {F ↾}_{(dom F \cap A)}$
5		resdm	$⊢ Rel F \to {F ↾}_{dom F} = F$
6	5	reseq1d	$⊢ Rel F \to {({F ↾}_{dom F}) ↾}_{A} = {F ↾}_{A}$
7	4 6	eqtr3id	$⊢ Rel F \to {F ↾}_{(dom F \cap A)} = {F ↾}_{A}$
8	7	rneqd	$⊢ Rel F \to ran ({F ↾}_{(dom F \cap A)}) = ran ({F ↾}_{A})$
9	3 8	eqtr4id	$⊢ Rel F \to F [A] = ran ({F ↾}_{(dom F \cap A)})$
10	1 2 9	3syl	$⊢ ((U \in Univ \land Fun F \land F [A] \subseteq U) \land A \in U) \to F [A] = ran ({F ↾}_{(dom F \cap A)})$
11		simpl1	$⊢ ((U \in Univ \land Fun F \land F [A] \subseteq U) \land A \in U) \to U \in Univ$
12		simpr	$⊢ ((U \in Univ \land Fun F \land F [A] \subseteq U) \land A \in U) \to A \in U$
13		inss2	$⊢ dom F \cap A \subseteq A$
14	13	a1i	$⊢ ((U \in Univ \land Fun F \land F [A] \subseteq U) \land A \in U) \to dom F \cap A \subseteq A$
15		gruss	$⊢ (U \in Univ \land A \in U \land dom F \cap A \subseteq A) \to dom F \cap A \in U$
16	11 12 14 15	syl3anc	$⊢ ((U \in Univ \land Fun F \land F [A] \subseteq U) \land A \in U) \to dom F \cap A \in U$
17		funforn	$⊢ Fun F \leftrightarrow F : dom F \underset{onto}{⟶} ran F$
18		fof	$⊢ F : dom F \underset{onto}{⟶} ran F \to F : dom F ⟶ ran F$
19	17 18	sylbi	$⊢ Fun F \to F : dom F ⟶ ran F$
20		inss1	$⊢ dom F \cap A \subseteq dom F$
21		fssres	$⊢ (F : dom F ⟶ ran F \land dom F \cap A \subseteq dom F) \to ({F ↾}_{(dom F \cap A)}) : dom F \cap A ⟶ ran F$
22	19 20 21	sylancl	$⊢ Fun F \to ({F ↾}_{(dom F \cap A)}) : dom F \cap A ⟶ ran F$
23		ffn	$⊢ ({F ↾}_{(dom F \cap A)}) : dom F \cap A ⟶ ran F \to ({F ↾}_{(dom F \cap A)}) Fn (dom F \cap A)$
24	1 22 23	3syl	$⊢ ((U \in Univ \land Fun F \land F [A] \subseteq U) \land A \in U) \to ({F ↾}_{(dom F \cap A)}) Fn (dom F \cap A)$
25		simpl3	$⊢ ((U \in Univ \land Fun F \land F [A] \subseteq U) \land A \in U) \to F [A] \subseteq U$
26	10 25	eqsstrrd	$⊢ ((U \in Univ \land Fun F \land F [A] \subseteq U) \land A \in U) \to ran ({F ↾}_{(dom F \cap A)}) \subseteq U$
27		df-f	$⊢ ({F ↾}_{(dom F \cap A)}) : dom F \cap A ⟶ U \leftrightarrow (({F ↾}_{(dom F \cap A)}) Fn (dom F \cap A) \land ran ({F ↾}_{(dom F \cap A)}) \subseteq U)$
28	24 26 27	sylanbrc	$⊢ ((U \in Univ \land Fun F \land F [A] \subseteq U) \land A \in U) \to ({F ↾}_{(dom F \cap A)}) : dom F \cap A ⟶ U$
29		grurn	$⊢ (U \in Univ \land dom F \cap A \in U \land ({F ↾}_{(dom F \cap A)}) : dom F \cap A ⟶ U) \to ran ({F ↾}_{(dom F \cap A)}) \in U$
30	11 16 28 29	syl3anc	$⊢ ((U \in Univ \land Fun F \land F [A] \subseteq U) \land A \in U) \to ran ({F ↾}_{(dom F \cap A)}) \in U$
31	10 30	eqeltrd	$⊢ ((U \in Univ \land Fun F \land F [A] \subseteq U) \land A \in U) \to F [A] \in U$
32	31	ex	$⊢ (U \in Univ \land Fun F \land F [A] \subseteq U) \to (A \in U \to F [A] \in U)$

Metamath Proof Explorer

Theorem gruima

Proof