sscfn1

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

	Ref	Expression
Hypotheses	sscfn1.1	$⊢ φ \to H \subseteq_{cat} J$
	sscfn1.2	$⊢ φ \to S = dom dom H$
Assertion	sscfn1	$⊢ φ \to H Fn (S \times S)$

Proof

Step	Hyp	Ref	Expression
1		sscfn1.1	$⊢ φ \to H \subseteq_{cat} J$
2		sscfn1.2	$⊢ φ \to S = dom dom H$
3		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))$
4	1 3	sylib	$⊢ φ \to \exists t (J Fn (t \times t) \land \exists s \in 𝒫 t H \in \underset{x \in s \times s}{⨉} 𝒫 J (x))$
5		ixpfn	$⊢ H \in \underset{x \in s \times s}{⨉} 𝒫 J (x) \to H Fn (s \times s)$
6		simpr	$⊢ (φ \land H Fn (s \times s)) \to H Fn (s \times s)$
7	2	adantr	$⊢ (φ \land H Fn (s \times s)) \to S = dom dom H$
8		fndm	$⊢ H Fn (s \times s) \to dom H = s \times s$
9	8	adantl	$⊢ (φ \land H Fn (s \times s)) \to dom H = s \times s$
10	9	dmeqd	$⊢ (φ \land H Fn (s \times s)) \to dom dom H = dom (s \times s)$
11		dmxpid	$⊢ dom (s \times s) = s$
12	10 11	eqtrdi	$⊢ (φ \land H Fn (s \times s)) \to dom dom H = s$
13	7 12	eqtr2d	$⊢ (φ \land H Fn (s \times s)) \to s = S$
14	13	sqxpeqd	$⊢ (φ \land H Fn (s \times s)) \to s \times s = S \times S$
15	14	fneq2d	$⊢ (φ \land H Fn (s \times s)) \to (H Fn (s \times s) \leftrightarrow H Fn (S \times S))$
16	6 15	mpbid	$⊢ (φ \land H Fn (s \times s)) \to H Fn (S \times S)$
17	16	ex	$⊢ φ \to (H Fn (s \times s) \to H Fn (S \times S))$
18	5 17	syl5	$⊢ φ \to (H \in \underset{x \in s \times s}{⨉} 𝒫 J (x) \to H Fn (S \times S))$
19	18	rexlimdvw	$⊢ φ \to (\exists s \in 𝒫 t H \in \underset{x \in s \times s}{⨉} 𝒫 J (x) \to H Fn (S \times S))$
20	19	adantld	$⊢ φ \to ((J Fn (t \times t) \land \exists s \in 𝒫 t H \in \underset{x \in s \times s}{⨉} 𝒫 J (x)) \to H Fn (S \times S))$
21	20	exlimdv	$⊢ φ \to (\exists t (J Fn (t \times t) \land \exists s \in 𝒫 t H \in \underset{x \in s \times s}{⨉} 𝒫 J (x)) \to H Fn (S \times S))$
22	4 21	mpd	$⊢ φ \to H Fn (S \times S)$

Metamath Proof Explorer

Theorem sscfn1

Proof