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

Metamath Proof Explorer

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 ( 𝑇 × 𝑇 ) )