sscpwex

Description: An analogue of pwex for the subcategory subset relation: The collection of subcategory subsets of a given set J is a set. (Contributed by Mario Carneiro, 6-Jan-2017)

		Ref	Expression
	Assertion	sscpwex	$⊢ \{h \| h \subseteq_{cat} J\} \in V$

Proof

Step	Hyp	Ref	Expression
1		ovex	$⊢ 𝒫 ⋃ ran J ↑_{𝑝𝑚} dom J \in V$
2		brssc	$⊢ h \subseteq_{cat} J \leftrightarrow \exists t (J Fn (t \times t) \land \exists s \in 𝒫 t h \in \underset{x \in s \times s}{⨉} 𝒫 J (x))$
3		simpl	$⊢ (J Fn (t \times t) \land (s \in 𝒫 t \land h \in \underset{x \in s \times s}{⨉} 𝒫 J (x))) \to J Fn (t \times t)$
4		vex	$⊢ t \in V$
5	4 4	xpex	$⊢ t \times t \in V$
6		fnex	$⊢ (J Fn (t \times t) \land t \times t \in V) \to J \in V$
7	3 5 6	sylancl	$⊢ (J Fn (t \times t) \land (s \in 𝒫 t \land h \in \underset{x \in s \times s}{⨉} 𝒫 J (x))) \to J \in V$
8		rnexg	$⊢ J \in V \to ran J \in V$
9		uniexg	$⊢ ran J \in V \to ⋃ ran J \in V$
10		pwexg	$⊢ ⋃ ran J \in V \to 𝒫 ⋃ ran J \in V$
11	7 8 9 10	4syl	$⊢ (J Fn (t \times t) \land (s \in 𝒫 t \land h \in \underset{x \in s \times s}{⨉} 𝒫 J (x))) \to 𝒫 ⋃ ran J \in V$
12		fndm	$⊢ J Fn (t \times t) \to dom J = t \times t$
13	12	adantr	$⊢ (J Fn (t \times t) \land (s \in 𝒫 t \land h \in \underset{x \in s \times s}{⨉} 𝒫 J (x))) \to dom J = t \times t$
14	13 5	eqeltrdi	$⊢ (J Fn (t \times t) \land (s \in 𝒫 t \land h \in \underset{x \in s \times s}{⨉} 𝒫 J (x))) \to dom J \in V$
15		ss2ixp	$⊢ \forall x \in (s \times s) 𝒫 J (x) \subseteq 𝒫 ⋃ ran J \to \underset{x \in s \times s}{⨉} 𝒫 J (x) \subseteq \underset{x \in s \times s}{⨉} 𝒫 ⋃ ran J$
16		fvssunirn	$⊢ J (x) \subseteq ⋃ ran J$
17	16	sspwi	$⊢ 𝒫 J (x) \subseteq 𝒫 ⋃ ran J$
18	17	a1i	$⊢ x \in (s \times s) \to 𝒫 J (x) \subseteq 𝒫 ⋃ ran J$
19	15 18	mprg	$⊢ \underset{x \in s \times s}{⨉} 𝒫 J (x) \subseteq \underset{x \in s \times s}{⨉} 𝒫 ⋃ ran J$
20		simprr	$⊢ (J Fn (t \times t) \land (s \in 𝒫 t \land h \in \underset{x \in s \times s}{⨉} 𝒫 J (x))) \to h \in \underset{x \in s \times s}{⨉} 𝒫 J (x)$
21	19 20	sseldi	$⊢ (J Fn (t \times t) \land (s \in 𝒫 t \land h \in \underset{x \in s \times s}{⨉} 𝒫 J (x))) \to h \in \underset{x \in s \times s}{⨉} 𝒫 ⋃ ran J$
22		vex	$⊢ h \in V$
23	22	elixpconst	$⊢ h \in \underset{x \in s \times s}{⨉} 𝒫 ⋃ ran J \leftrightarrow h : s \times s ⟶ 𝒫 ⋃ ran J$
24	21 23	sylib	$⊢ (J Fn (t \times t) \land (s \in 𝒫 t \land h \in \underset{x \in s \times s}{⨉} 𝒫 J (x))) \to h : s \times s ⟶ 𝒫 ⋃ ran J$
25		elpwi	$⊢ s \in 𝒫 t \to s \subseteq t$
26	25	ad2antrl	$⊢ (J Fn (t \times t) \land (s \in 𝒫 t \land h \in \underset{x \in s \times s}{⨉} 𝒫 J (x))) \to s \subseteq t$
27		xpss12	$⊢ (s \subseteq t \land s \subseteq t) \to s \times s \subseteq t \times t$
28	26 26 27	syl2anc	$⊢ (J Fn (t \times t) \land (s \in 𝒫 t \land h \in \underset{x \in s \times s}{⨉} 𝒫 J (x))) \to s \times s \subseteq t \times t$
29	28 13	sseqtrrd	$⊢ (J Fn (t \times t) \land (s \in 𝒫 t \land h \in \underset{x \in s \times s}{⨉} 𝒫 J (x))) \to s \times s \subseteq dom J$
30		elpm2r	$⊢ ((𝒫 ⋃ ran J \in V \land dom J \in V) \land (h : s \times s ⟶ 𝒫 ⋃ ran J \land s \times s \subseteq dom J)) \to h \in (𝒫 ⋃ ran J ↑_{𝑝𝑚} dom J)$
31	11 14 24 29 30	syl22anc	$⊢ (J Fn (t \times t) \land (s \in 𝒫 t \land h \in \underset{x \in s \times s}{⨉} 𝒫 J (x))) \to h \in (𝒫 ⋃ ran J ↑_{𝑝𝑚} dom J)$
32	31	rexlimdvaa	$⊢ J Fn (t \times t) \to (\exists s \in 𝒫 t h \in \underset{x \in s \times s}{⨉} 𝒫 J (x) \to h \in (𝒫 ⋃ ran J ↑_{𝑝𝑚} dom J))$
33	32	imp	$⊢ (J Fn (t \times t) \land \exists s \in 𝒫 t h \in \underset{x \in s \times s}{⨉} 𝒫 J (x)) \to h \in (𝒫 ⋃ ran J ↑_{𝑝𝑚} dom J)$
34	33	exlimiv	$⊢ \exists t (J Fn (t \times t) \land \exists s \in 𝒫 t h \in \underset{x \in s \times s}{⨉} 𝒫 J (x)) \to h \in (𝒫 ⋃ ran J ↑_{𝑝𝑚} dom J)$
35	2 34	sylbi	$⊢ h \subseteq_{cat} J \to h \in (𝒫 ⋃ ran J ↑_{𝑝𝑚} dom J)$
36	35	abssi	$⊢ \{h \| h \subseteq_{cat} J\} \subseteq 𝒫 ⋃ ran J ↑_{𝑝𝑚} dom J$
37	1 36	ssexi	$⊢ \{h \| h \subseteq_{cat} J\} \in V$

Metamath Proof Explorer

Theorem sscpwex

Proof