Theorem sscfn2

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 𝐽 )
	sscfn2.2	⊢ ( 𝜑 → 𝑇 = dom dom 𝐽 )
Assertion	sscfn2	⊢ ( 𝜑 → 𝐽 Fn ( 𝑇 × 𝑇 ) )

Proof

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