sscfn2

Description: The subcategory subset relation is defined on functions with square domain. (Contributed by Mario Carneiro, 6-Jan-2017)

Step	Hyp	Ref	Expression
1		sscfn1.1	$⊢ φ \to H \subseteq_{cat} J$
2		sscfn2.2	$⊢ φ \to T = dom dom J$
3		brssc	$⊢ H \subseteq_{cat} J \leftrightarrow \exists t (J Fn (t \times t) \land \exists y \in 𝒫 t H \in \underset{x \in y \times y}{⨉} 𝒫 J (x))$
4	1 3	sylib	$⊢ φ \to \exists t (J Fn (t \times t) \land \exists y \in 𝒫 t H \in \underset{x \in y \times y}{⨉} 𝒫 J (x))$
5		simpr	$⊢ (φ \land J Fn (t \times t)) \to J Fn (t \times t)$
6	2	adantr	$⊢ (φ \land J Fn (t \times t)) \to T = dom dom J$
7		fndm	$⊢ J Fn (t \times t) \to dom J = t \times t$
8	7	adantl	$⊢ (φ \land J Fn (t \times t)) \to dom J = t \times t$
9	8	dmeqd	$⊢ (φ \land J Fn (t \times t)) \to dom dom J = dom (t \times t)$
10		dmxpid	$⊢ dom (t \times t) = t$
11	9 10	eqtrdi	$⊢ (φ \land J Fn (t \times t)) \to dom dom J = t$
12	6 11	eqtr2d	$⊢ (φ \land J Fn (t \times t)) \to t = T$
13	12	sqxpeqd	$⊢ (φ \land J Fn (t \times t)) \to t \times t = T \times T$
14	13	fneq2d	$⊢ (φ \land J Fn (t \times t)) \to (J Fn (t \times t) \leftrightarrow J Fn (T \times T))$
15	5 14	mpbid	$⊢ (φ \land J Fn (t \times t)) \to J Fn (T \times T)$
16	15	ex	$⊢ φ \to (J Fn (t \times t) \to J Fn (T \times T))$
17	16	adantrd	$⊢ φ \to ((J Fn (t \times t) \land \exists y \in 𝒫 t H \in \underset{x \in y \times y}{⨉} 𝒫 J (x)) \to J Fn (T \times T))$
18	17	exlimdv	$⊢ φ \to (\exists t (J Fn (t \times t) \land \exists y \in 𝒫 t H \in \underset{x \in y \times y}{⨉} 𝒫 J (x)) \to J Fn (T \times T))$
19	4 18	mpd	$⊢ φ \to J Fn (T \times T)$

Metamath Proof Explorer