ingru

Description: The intersection of a universe with a class that acts like a universe is another universe. (Contributed by Mario Carneiro, 10-Jun-2013)

		Ref	Expression
	Assertion	ingru	$⊢ (Tr A \land \forall x \in A (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A))) \to (U \in Univ \to U \cap A \in Univ)$

Proof

Step	Hyp	Ref	Expression
1		ineq1	$⊢ u = U \to u \cap A = U \cap A$
2	1	eleq1d	$⊢ u = U \to (u \cap A \in Univ \leftrightarrow U \cap A \in Univ)$
3	2	imbi2d	$⊢ u = U \to (((Tr A \land \forall x \in A (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A))) \to u \cap A \in Univ) \leftrightarrow ((Tr A \land \forall x \in A (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A))) \to U \cap A \in Univ))$
4		elgrug	$⊢ u \in Univ \to (u \in Univ \leftrightarrow (Tr u \land \forall x \in u (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u)))$
5	4	ibi	$⊢ u \in Univ \to (Tr u \land \forall x \in u (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u))$
6		trin	$⊢ (Tr u \land Tr A) \to Tr (u \cap A)$
7	6	ex	$⊢ Tr u \to (Tr A \to Tr (u \cap A))$
8		inss1	$⊢ u \cap A \subseteq u$
9		ssralv	$⊢ u \cap A \subseteq u \to (\forall x \in u (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u) \to \forall x \in (u \cap A) (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u))$
10	8 9	ax-mp	$⊢ \forall x \in u (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u) \to \forall x \in (u \cap A) (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u)$
11		inss2	$⊢ u \cap A \subseteq A$
12		ssralv	$⊢ u \cap A \subseteq A \to (\forall x \in A (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A)) \to \forall x \in (u \cap A) (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A)))$
13	11 12	ax-mp	$⊢ \forall x \in A (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A)) \to \forall x \in (u \cap A) (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A))$
14		elin	$⊢ 𝒫 x \in (u \cap A) \leftrightarrow (𝒫 x \in u \land 𝒫 x \in A)$
15	14	simplbi2	$⊢ 𝒫 x \in u \to (𝒫 x \in A \to 𝒫 x \in (u \cap A))$
16		ssralv	$⊢ u \cap A \subseteq u \to (\forall y \in u \{x, y\} \in u \to \forall y \in (u \cap A) \{x, y\} \in u)$
17	8 16	ax-mp	$⊢ \forall y \in u \{x, y\} \in u \to \forall y \in (u \cap A) \{x, y\} \in u$
18		ssralv	$⊢ u \cap A \subseteq A \to (\forall y \in A \{x, y\} \in A \to \forall y \in (u \cap A) \{x, y\} \in A)$
19	11 18	ax-mp	$⊢ \forall y \in A \{x, y\} \in A \to \forall y \in (u \cap A) \{x, y\} \in A$
20		elin	$⊢ \{x, y\} \in (u \cap A) \leftrightarrow (\{x, y\} \in u \land \{x, y\} \in A)$
21	20	simplbi2	$⊢ \{x, y\} \in u \to (\{x, y\} \in A \to \{x, y\} \in (u \cap A))$
22	21	ral2imi	$⊢ \forall y \in (u \cap A) \{x, y\} \in u \to (\forall y \in (u \cap A) \{x, y\} \in A \to \forall y \in (u \cap A) \{x, y\} \in (u \cap A))$
23	17 19 22	syl2im	$⊢ \forall y \in u \{x, y\} \in u \to (\forall y \in A \{x, y\} \in A \to \forall y \in (u \cap A) \{x, y\} \in (u \cap A))$
24	15 23	im2anan9	$⊢ (𝒫 x \in u \land \forall y \in u \{x, y\} \in u) \to ((𝒫 x \in A \land \forall y \in A \{x, y\} \in A) \to (𝒫 x \in (u \cap A) \land \forall y \in (u \cap A) \{x, y\} \in (u \cap A)))$
25		vex	$⊢ u \in V$
26		mapss	$⊢ (u \in V \land u \cap A \subseteq u) \to {(u \cap A)}^{x} \subseteq u^{x}$
27	25 8 26	mp2an	$⊢ {(u \cap A)}^{x} \subseteq u^{x}$
28		ssralv	$⊢ {(u \cap A)}^{x} \subseteq u^{x} \to (\forall y \in (u^{x}) ⋃ ran y \in u \to \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in u)$
29	27 28	ax-mp	$⊢ \forall y \in (u^{x}) ⋃ ran y \in u \to \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in u$
30	25	inex1	$⊢ u \cap A \in V$
31		vex	$⊢ x \in V$
32	30 31	elmap	$⊢ y \in ({(u \cap A)}^{x}) \leftrightarrow y : x ⟶ u \cap A$
33		fss	$⊢ (y : x ⟶ u \cap A \land u \cap A \subseteq A) \to y : x ⟶ A$
34	11 33	mpan2	$⊢ y : x ⟶ u \cap A \to y : x ⟶ A$
35	32 34	sylbi	$⊢ y \in ({(u \cap A)}^{x}) \to y : x ⟶ A$
36	35	imim1i	$⊢ (y : x ⟶ A \to ⋃ ran y \in A) \to (y \in ({(u \cap A)}^{x}) \to ⋃ ran y \in A)$
37	36	alimi	$⊢ \forall y (y : x ⟶ A \to ⋃ ran y \in A) \to \forall y (y \in ({(u \cap A)}^{x}) \to ⋃ ran y \in A)$
38		df-ral	$⊢ \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in A \leftrightarrow \forall y (y \in ({(u \cap A)}^{x}) \to ⋃ ran y \in A)$
39	37 38	sylibr	$⊢ \forall y (y : x ⟶ A \to ⋃ ran y \in A) \to \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in A$
40		elin	$⊢ ⋃ ran y \in (u \cap A) \leftrightarrow (⋃ ran y \in u \land ⋃ ran y \in A)$
41	40	simplbi2	$⊢ ⋃ ran y \in u \to (⋃ ran y \in A \to ⋃ ran y \in (u \cap A))$
42	41	ral2imi	$⊢ \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in u \to (\forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in A \to \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in (u \cap A))$
43	29 39 42	syl2im	$⊢ \forall y \in (u^{x}) ⋃ ran y \in u \to (\forall y (y : x ⟶ A \to ⋃ ran y \in A) \to \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in (u \cap A))$
44	24 43	im2anan9	$⊢ ((𝒫 x \in u \land \forall y \in u \{x, y\} \in u) \land \forall y \in (u^{x}) ⋃ ran y \in u) \to (((𝒫 x \in A \land \forall y \in A \{x, y\} \in A) \land \forall y (y : x ⟶ A \to ⋃ ran y \in A)) \to ((𝒫 x \in (u \cap A) \land \forall y \in (u \cap A) \{x, y\} \in (u \cap A)) \land \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in (u \cap A)))$
45	44	3impa	$⊢ (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u) \to (((𝒫 x \in A \land \forall y \in A \{x, y\} \in A) \land \forall y (y : x ⟶ A \to ⋃ ran y \in A)) \to ((𝒫 x \in (u \cap A) \land \forall y \in (u \cap A) \{x, y\} \in (u \cap A)) \land \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in (u \cap A)))$
46		df-3an	$⊢ (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A)) \leftrightarrow ((𝒫 x \in A \land \forall y \in A \{x, y\} \in A) \land \forall y (y : x ⟶ A \to ⋃ ran y \in A))$
47		df-3an	$⊢ (𝒫 x \in (u \cap A) \land \forall y \in (u \cap A) \{x, y\} \in (u \cap A) \land \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in (u \cap A)) \leftrightarrow ((𝒫 x \in (u \cap A) \land \forall y \in (u \cap A) \{x, y\} \in (u \cap A)) \land \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in (u \cap A))$
48	45 46 47	3imtr4g	$⊢ (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u) \to ((𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A)) \to (𝒫 x \in (u \cap A) \land \forall y \in (u \cap A) \{x, y\} \in (u \cap A) \land \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in (u \cap A)))$
49	48	ral2imi	$⊢ \forall x \in (u \cap A) (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u) \to (\forall x \in (u \cap A) (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A)) \to \forall x \in (u \cap A) (𝒫 x \in (u \cap A) \land \forall y \in (u \cap A) \{x, y\} \in (u \cap A) \land \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in (u \cap A)))$
50	10 13 49	syl2im	$⊢ \forall x \in u (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u) \to (\forall x \in A (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A)) \to \forall x \in (u \cap A) (𝒫 x \in (u \cap A) \land \forall y \in (u \cap A) \{x, y\} \in (u \cap A) \land \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in (u \cap A)))$
51	7 50	im2anan9	$⊢ (Tr u \land \forall x \in u (𝒫 x \in u \land \forall y \in u \{x, y\} \in u \land \forall y \in (u^{x}) ⋃ ran y \in u)) \to ((Tr A \land \forall x \in A (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A))) \to (Tr (u \cap A) \land \forall x \in (u \cap A) (𝒫 x \in (u \cap A) \land \forall y \in (u \cap A) \{x, y\} \in (u \cap A) \land \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in (u \cap A))))$
52	5 51	syl	$⊢ u \in Univ \to ((Tr A \land \forall x \in A (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A))) \to (Tr (u \cap A) \land \forall x \in (u \cap A) (𝒫 x \in (u \cap A) \land \forall y \in (u \cap A) \{x, y\} \in (u \cap A) \land \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in (u \cap A))))$
53		elgrug	$⊢ u \cap A \in V \to (u \cap A \in Univ \leftrightarrow (Tr (u \cap A) \land \forall x \in (u \cap A) (𝒫 x \in (u \cap A) \land \forall y \in (u \cap A) \{x, y\} \in (u \cap A) \land \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in (u \cap A))))$
54	30 53	ax-mp	$⊢ u \cap A \in Univ \leftrightarrow (Tr (u \cap A) \land \forall x \in (u \cap A) (𝒫 x \in (u \cap A) \land \forall y \in (u \cap A) \{x, y\} \in (u \cap A) \land \forall y \in ({(u \cap A)}^{x}) ⋃ ran y \in (u \cap A)))$
55	52 54	imbitrrdi	$⊢ u \in Univ \to ((Tr A \land \forall x \in A (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A))) \to u \cap A \in Univ)$
56	3 55	vtoclga	$⊢ U \in Univ \to ((Tr A \land \forall x \in A (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A))) \to U \cap A \in Univ)$
57	56	com12	$⊢ (Tr A \land \forall x \in A (𝒫 x \in A \land \forall y \in A \{x, y\} \in A \land \forall y (y : x ⟶ A \to ⋃ ran y \in A))) \to (U \in Univ \to U \cap A \in Univ)$

Metamath Proof Explorer

Theorem ingru

Proof