brssc

Description: The subcategory subset relation is a relation. (Contributed by Mario Carneiro, 6-Jan-2017)

		Ref	Expression
	Assertion	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))$

Proof

Step	Hyp	Ref	Expression
1		sscrel	$⊢ Rel \subseteq_{cat}$
2	1	brrelex12i	$⊢ H \subseteq_{cat} J \to (H \in V \land J \in V)$
3		vex	$⊢ t \in V$
4	3 3	xpex	$⊢ t \times t \in V$
5		fnex	$⊢ (J Fn (t \times t) \land t \times t \in V) \to J \in V$
6	4 5	mpan2	$⊢ J Fn (t \times t) \to J \in V$
7		elex	$⊢ H \in \underset{x \in s \times s}{⨉} 𝒫 J (x) \to H \in V$
8	7	rexlimivw	$⊢ \exists s \in 𝒫 t H \in \underset{x \in s \times s}{⨉} 𝒫 J (x) \to H \in V$
9	6 8	anim12ci	$⊢ (J Fn (t \times t) \land \exists s \in 𝒫 t H \in \underset{x \in s \times s}{⨉} 𝒫 J (x)) \to (H \in V \land J \in V)$
10	9	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 V \land J \in V)$
11		simpr	$⊢ (h = H \land j = J) \to j = J$
12	11	fneq1d	$⊢ (h = H \land j = J) \to (j Fn (t \times t) \leftrightarrow J Fn (t \times t))$
13		simpl	$⊢ (h = H \land j = J) \to h = H$
14	11	fveq1d	$⊢ (h = H \land j = J) \to j (x) = J (x)$
15	14	pweqd	$⊢ (h = H \land j = J) \to 𝒫 j (x) = 𝒫 J (x)$
16	15	ixpeq2dv	$⊢ (h = H \land j = J) \to \underset{x \in s \times s}{⨉} 𝒫 j (x) = \underset{x \in s \times s}{⨉} 𝒫 J (x)$
17	13 16	eleq12d	$⊢ (h = H \land j = J) \to (h \in \underset{x \in s \times s}{⨉} 𝒫 j (x) \leftrightarrow H \in \underset{x \in s \times s}{⨉} 𝒫 J (x))$
18	17	rexbidv	$⊢ (h = H \land j = J) \to (\exists s \in 𝒫 t h \in \underset{x \in s \times s}{⨉} 𝒫 j (x) \leftrightarrow \exists s \in 𝒫 t H \in \underset{x \in s \times s}{⨉} 𝒫 J (x))$
19	12 18	anbi12d	$⊢ (h = H \land j = J) \to ((j Fn (t \times t) \land \exists s \in 𝒫 t h \in \underset{x \in s \times s}{⨉} 𝒫 j (x)) \leftrightarrow (J Fn (t \times t) \land \exists s \in 𝒫 t H \in \underset{x \in s \times s}{⨉} 𝒫 J (x)))$
20	19	exbidv	$⊢ (h = H \land j = J) \to (\exists t (j Fn (t \times t) \land \exists s \in 𝒫 t h \in \underset{x \in s \times s}{⨉} 𝒫 j (x)) \leftrightarrow \exists t (J Fn (t \times t) \land \exists s \in 𝒫 t H \in \underset{x \in s \times s}{⨉} 𝒫 J (x)))$
21		df-ssc	$⊢ \subseteq_{cat} = \{⟨h, j⟩ \| \exists t (j Fn (t \times t) \land \exists s \in 𝒫 t h \in \underset{x \in s \times s}{⨉} 𝒫 j (x))\}$
22	20 21	brabga	$⊢ (H \in V \land J \in V) \to (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)))$
23	2 10 22	pm5.21nii	$⊢ 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))$

Metamath Proof Explorer

Theorem brssc

Proof