This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐻 ⊆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 ( 𝑆 × 𝑆 ) )