Metamath Proof Explorer

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 ⊢ φ → H ⊆ cat J
sscfn1.2 ⊢ φ → S = dom ⁡ dom ⁡ H
Assertion sscfn1 ⊢ φ → H Fn S × S

Proof

Step Hyp Ref Expression
1 sscfn1.1 ⊢ φ → H ⊆ cat J
2 sscfn1.2 ⊢ φ → S = dom ⁡ dom ⁡ H
3 brssc ⊢ H ⊆ cat J ↔ ∃ t J Fn t × t ∧ ∃ s ∈ 𝒫 t H ∈ ⨉ x ∈ s × s 𝒫 J ⁡ x
4 1 3 sylib ⊢ φ → ∃ t J Fn t × t ∧ ∃ s ∈ 𝒫 t H ∈ ⨉ x ∈ s × s 𝒫 J ⁡ x
5 ixpfn ⊢ H ∈ ⨉ x ∈ s × s 𝒫 J ⁡ x → H Fn s × s
6 simpr ⊢ φ ∧ H Fn s × s → H Fn s × s
7 2 adantr ⊢ φ ∧ H Fn s × s → S = dom ⁡ dom ⁡ H
8 fndm ⊢ H Fn s × s → dom ⁡ H = s × s
9 8 adantl ⊢ φ ∧ H Fn s × s → dom ⁡ H = s × s
10 9 dmeqd ⊢ φ ∧ H Fn s × s → dom ⁡ dom ⁡ H = dom ⁡ s × s
11 dmxpid ⊢ dom ⁡ s × s = s
12 10 11 eqtrdi ⊢ φ ∧ H Fn s × s → dom ⁡ dom ⁡ H = s
13 7 12 eqtr2d ⊢ φ ∧ H Fn s × s → s = S
14 13 sqxpeqd ⊢ φ ∧ H Fn s × s → s × s = S × S
15 14 fneq2d ⊢ φ ∧ H Fn s × s → H Fn s × s ↔ H Fn S × S
16 6 15 mpbid ⊢ φ ∧ H Fn s × s → H Fn S × S
17 16 ex ⊢ φ → H Fn s × s → H Fn S × S
18 5 17 syl5 ⊢ φ → H ∈ ⨉ x ∈ s × s 𝒫 J ⁡ x → H Fn S × S
19 18 rexlimdvw ⊢ φ → ∃ s ∈ 𝒫 t H ∈ ⨉ x ∈ s × s 𝒫 J ⁡ x → H Fn S × S
20 19 adantld ⊢ φ → J Fn t × t ∧ ∃ s ∈ 𝒫 t H ∈ ⨉ x ∈ s × s 𝒫 J ⁡ x → H Fn S × S
21 20 exlimdv ⊢ φ → ∃ t J Fn t × t ∧ ∃ s ∈ 𝒫 t H ∈ ⨉ x ∈ s × s 𝒫 J ⁡ x → H Fn S × S
22 4 21 mpd ⊢ φ → H Fn S × S