Theorem 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	⊢ ( 𝜑 → 𝐻 ⊆cat 𝐽 )
	sscfn1.2	⊢ ( 𝜑 → 𝑆 = dom dom 𝐻 )
Assertion	sscfn1	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		sscfn1.1	⊢ ( 𝜑 → 𝐻 ⊆cat 𝐽 )
2		sscfn1.2	⊢ ( 𝜑 → 𝑆 = dom dom 𝐻 )
3		brssc	⊢ ( 𝐻 ⊆cat 𝐽 ↔ ∃ 𝑡 ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) )
4	1 3	sylib	⊢ ( 𝜑 → ∃ 𝑡 ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) )
5		ixpfn	⊢ ( 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) → 𝐻 Fn ( 𝑠 × 𝑠 ) )
6		simpr	⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → 𝐻 Fn ( 𝑠 × 𝑠 ) )
7	2	adantr	⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → 𝑆 = dom dom 𝐻 )
8		fndm	⊢ ( 𝐻 Fn ( 𝑠 × 𝑠 ) → dom 𝐻 = ( 𝑠 × 𝑠 ) )
9	8	adantl	⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → dom 𝐻 = ( 𝑠 × 𝑠 ) )
10	9	dmeqd	⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → dom dom 𝐻 = dom ( 𝑠 × 𝑠 ) )
11		dmxpid	⊢ dom ( 𝑠 × 𝑠 ) = 𝑠
12	10 11	eqtrdi	⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → dom dom 𝐻 = 𝑠 )
13	7 12	eqtr2d	⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → 𝑠 = 𝑆 )
14	13	sqxpeqd	⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → ( 𝑠 × 𝑠 ) = ( 𝑆 × 𝑆 ) )
15	14	fneq2d	⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → ( 𝐻 Fn ( 𝑠 × 𝑠 ) ↔ 𝐻 Fn ( 𝑆 × 𝑆 ) ) )
16	6 15	mpbid	⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → 𝐻 Fn ( 𝑆 × 𝑆 ) )
17	16	ex	⊢ ( 𝜑 → ( 𝐻 Fn ( 𝑠 × 𝑠 ) → 𝐻 Fn ( 𝑆 × 𝑆 ) ) )
18	5 17	syl5	⊢ ( 𝜑 → ( 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) → 𝐻 Fn ( 𝑆 × 𝑆 ) ) )
19	18	rexlimdvw	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) → 𝐻 Fn ( 𝑆 × 𝑆 ) ) )
20	19	adantld	⊢ ( 𝜑 → ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) → 𝐻 Fn ( 𝑆 × 𝑆 ) ) )
21	20	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑡 ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑥 ) ) → 𝐻 Fn ( 𝑆 × 𝑆 ) ) )
22	4 21	mpd	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )