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

Metamath Proof Explorer

Theorem isssc

Description: Value of the subcategory subset relation when the arguments are known functions. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Hypotheses isssc.1 ⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
isssc.2 ⊢ ( 𝜑 → 𝐽 Fn ( 𝑇 × 𝑇 ) )
isssc.3 ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
Assertion isssc ( 𝜑 → ( 𝐻 ⊆cat 𝐽 ↔ ( 𝑆 ⊆ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 isssc.1 ⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
2 isssc.2 ⊢ ( 𝜑 → 𝐽 Fn ( 𝑇 × 𝑇 ) )
3 isssc.3 ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
4 brssc ⊢ ( 𝐻 ⊆cat 𝐽 ↔ ∃ 𝑡 ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) )
5 fndm ⊢ ( 𝐽 Fn ( 𝑡 × 𝑡 ) → dom 𝐽 = ( 𝑡 × 𝑡 ) )
6 5 adantl ⊢ ( ( 𝜑 ∧ 𝐽 Fn ( 𝑡 × 𝑡 ) ) → dom 𝐽 = ( 𝑡 × 𝑡 ) )
7 2 adantr ⊢ ( ( 𝜑 ∧ 𝐽 Fn ( 𝑡 × 𝑡 ) ) → 𝐽 Fn ( 𝑇 × 𝑇 ) )
8 7 fndmd ⊢ ( ( 𝜑 ∧ 𝐽 Fn ( 𝑡 × 𝑡 ) ) → dom 𝐽 = ( 𝑇 × 𝑇 ) )
9 6 8 eqtr3d ⊢ ( ( 𝜑 ∧ 𝐽 Fn ( 𝑡 × 𝑡 ) ) → ( 𝑡 × 𝑡 ) = ( 𝑇 × 𝑇 ) )
10 9 dmeqd ⊢ ( ( 𝜑 ∧ 𝐽 Fn ( 𝑡 × 𝑡 ) ) → dom ( 𝑡 × 𝑡 ) = dom ( 𝑇 × 𝑇 ) )
11 dmxpid ⊢ dom ( 𝑡 × 𝑡 ) = 𝑡
12 dmxpid ⊢ dom ( 𝑇 × 𝑇 ) = 𝑇
13 10 11 12 3eqtr3g ⊢ ( ( 𝜑 ∧ 𝐽 Fn ( 𝑡 × 𝑡 ) ) → 𝑡 = 𝑇 )
14 13 ex ⊢ ( 𝜑 → ( 𝐽 Fn ( 𝑡 × 𝑡 ) → 𝑡 = 𝑇 ) )
15 id ⊢ ( 𝑡 = 𝑇 → 𝑡 = 𝑇 )
16 15 sqxpeqd ⊢ ( 𝑡 = 𝑇 → ( 𝑡 × 𝑡 ) = ( 𝑇 × 𝑇 ) )
17 16 fneq2d ⊢ ( 𝑡 = 𝑇 → ( 𝐽 Fn ( 𝑡 × 𝑡 ) ↔ 𝐽 Fn ( 𝑇 × 𝑇 ) ) )
18 2 17 syl5ibrcom ⊢ ( 𝜑 → ( 𝑡 = 𝑇 → 𝐽 Fn ( 𝑡 × 𝑡 ) ) )
19 14 18 impbid ⊢ ( 𝜑 → ( 𝐽 Fn ( 𝑡 × 𝑡 ) ↔ 𝑡 = 𝑇 ) )
20 19 anbi1d ⊢ ( 𝜑 → ( ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) ↔ ( 𝑡 = 𝑇 ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) )
21 20 exbidv ⊢ ( 𝜑 → ( ∃ 𝑡 ( 𝐽 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) ↔ ∃ 𝑡 ( 𝑡 = 𝑇 ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) )
22 4 21 bitrid ⊢ ( 𝜑 → ( 𝐻 ⊆cat 𝐽 ↔ ∃ 𝑡 ( 𝑡 = 𝑇 ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) )
23 pweq ⊢ ( 𝑡 = 𝑇 → 𝒫 𝑡 = 𝒫 𝑇 )
24 23 rexeqdv ⊢ ( 𝑡 = 𝑇 → ( ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ↔ ∃ 𝑠 ∈ 𝒫 𝑇 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) )
25 24 ceqsexgv ⊢ ( 𝑇 ∈ 𝑉 → ( ∃ 𝑡 ( 𝑡 = 𝑇 ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) ↔ ∃ 𝑠 ∈ 𝒫 𝑇 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) )
26 3 25 syl ⊢ ( 𝜑 → ( ∃ 𝑡 ( 𝑡 = 𝑇 ∧ ∃ 𝑠 ∈ 𝒫 𝑡 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) ↔ ∃ 𝑠 ∈ 𝒫 𝑇 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) )
27 22 26 bitrd ⊢ ( 𝜑 → ( 𝐻 ⊆cat 𝐽 ↔ ∃ 𝑠 ∈ 𝒫 𝑇 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) )
28 df-rex ⊢ ( ∃ 𝑠 ∈ 𝒫 𝑇 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ↔ ∃ 𝑠 ( 𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) )
29 3anass ⊢ ( ( 𝐻 ∈ V ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ↔ ( 𝐻 ∈ V ∧ ( 𝐻 Fn ( 𝑠 × 𝑠 ) ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) )
30 elixp2 ⊢ ( 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ↔ ( 𝐻 ∈ V ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) )
31 vex ⊢ 𝑠 ∈ V
32 31 31 xpex ⊢ ( 𝑠 × 𝑠 ) ∈ V
33 fnex ⊢ ( ( 𝐻 Fn ( 𝑠 × 𝑠 ) ∧ ( 𝑠 × 𝑠 ) ∈ V ) → 𝐻 ∈ V )
34 32 33 mpan2 ⊢ ( 𝐻 Fn ( 𝑠 × 𝑠 ) → 𝐻 ∈ V )
35 34 adantr ⊢ ( ( 𝐻 Fn ( 𝑠 × 𝑠 ) ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) → 𝐻 ∈ V )
36 35 pm4.71ri ⊢ ( ( 𝐻 Fn ( 𝑠 × 𝑠 ) ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ↔ ( 𝐻 ∈ V ∧ ( 𝐻 Fn ( 𝑠 × 𝑠 ) ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) )
37 29 30 36 3bitr4i ⊢ ( 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ↔ ( 𝐻 Fn ( 𝑠 × 𝑠 ) ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) )
38 fndm ⊢ ( 𝐻 Fn ( 𝑠 × 𝑠 ) → dom 𝐻 = ( 𝑠 × 𝑠 ) )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → dom 𝐻 = ( 𝑠 × 𝑠 ) )
40 1 adantr ⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → 𝐻 Fn ( 𝑆 × 𝑆 ) )
41 40 fndmd ⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → dom 𝐻 = ( 𝑆 × 𝑆 ) )
42 39 41 eqtr3d ⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → ( 𝑠 × 𝑠 ) = ( 𝑆 × 𝑆 ) )
43 42 dmeqd ⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → dom ( 𝑠 × 𝑠 ) = dom ( 𝑆 × 𝑆 ) )
44 dmxpid ⊢ dom ( 𝑠 × 𝑠 ) = 𝑠
45 dmxpid ⊢ dom ( 𝑆 × 𝑆 ) = 𝑆
46 43 44 45 3eqtr3g ⊢ ( ( 𝜑 ∧ 𝐻 Fn ( 𝑠 × 𝑠 ) ) → 𝑠 = 𝑆 )
47 46 ex ⊢ ( 𝜑 → ( 𝐻 Fn ( 𝑠 × 𝑠 ) → 𝑠 = 𝑆 ) )
48 id ⊢ ( 𝑠 = 𝑆 → 𝑠 = 𝑆 )
49 48 sqxpeqd ⊢ ( 𝑠 = 𝑆 → ( 𝑠 × 𝑠 ) = ( 𝑆 × 𝑆 ) )
50 49 fneq2d ⊢ ( 𝑠 = 𝑆 → ( 𝐻 Fn ( 𝑠 × 𝑠 ) ↔ 𝐻 Fn ( 𝑆 × 𝑆 ) ) )
51 1 50 syl5ibrcom ⊢ ( 𝜑 → ( 𝑠 = 𝑆 → 𝐻 Fn ( 𝑠 × 𝑠 ) ) )
52 47 51 impbid ⊢ ( 𝜑 → ( 𝐻 Fn ( 𝑠 × 𝑠 ) ↔ 𝑠 = 𝑆 ) )
53 52 anbi1d ⊢ ( 𝜑 → ( ( 𝐻 Fn ( 𝑠 × 𝑠 ) ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ↔ ( 𝑠 = 𝑆 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) )
54 37 53 bitrid ⊢ ( 𝜑 → ( 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ↔ ( 𝑠 = 𝑆 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) )
55 54 anbi2d ⊢ ( 𝜑 → ( ( 𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) ↔ ( 𝑠 ∈ 𝒫 𝑇 ∧ ( 𝑠 = 𝑆 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) ) )
56 an12 ⊢ ( ( 𝑠 ∈ 𝒫 𝑇 ∧ ( 𝑠 = 𝑆 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) ↔ ( 𝑠 = 𝑆 ∧ ( 𝑠 ∈ 𝒫 𝑇 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) )
57 55 56 bitrdi ⊢ ( 𝜑 → ( ( 𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) ↔ ( 𝑠 = 𝑆 ∧ ( 𝑠 ∈ 𝒫 𝑇 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) ) )
58 57 exbidv ⊢ ( 𝜑 → ( ∃ 𝑠 ( 𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ) ↔ ∃ 𝑠 ( 𝑠 = 𝑆 ∧ ( 𝑠 ∈ 𝒫 𝑇 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) ) )
59 28 58 bitrid ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝒫 𝑇 𝐻 ∈ X 𝑧 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝐽 ‘ 𝑧 ) ↔ ∃ 𝑠 ( 𝑠 = 𝑆 ∧ ( 𝑠 ∈ 𝒫 𝑇 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) ) )
60 exsimpl ⊢ ( ∃ 𝑠 ( 𝑠 = 𝑆 ∧ ( 𝑠 ∈ 𝒫 𝑇 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) → ∃ 𝑠 𝑠 = 𝑆 )
61 isset ⊢ ( 𝑆 ∈ V ↔ ∃ 𝑠 𝑠 = 𝑆 )
62 60 61 sylibr ⊢ ( ∃ 𝑠 ( 𝑠 = 𝑆 ∧ ( 𝑠 ∈ 𝒫 𝑇 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) → 𝑆 ∈ V )
63 62 a1i ⊢ ( 𝜑 → ( ∃ 𝑠 ( 𝑠 = 𝑆 ∧ ( 𝑠 ∈ 𝒫 𝑇 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) → 𝑆 ∈ V ) )
64 ssexg ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑉 ) → 𝑆 ∈ V )
65 64 expcom ⊢ ( 𝑇 ∈ 𝑉 → ( 𝑆 ⊆ 𝑇 → 𝑆 ∈ V ) )
66 3 65 syl ⊢ ( 𝜑 → ( 𝑆 ⊆ 𝑇 → 𝑆 ∈ V ) )
67 66 adantrd ⊢ ( 𝜑 → ( ( 𝑆 ⊆ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) → 𝑆 ∈ V ) )
68 31 elpw ⊢ ( 𝑠 ∈ 𝒫 𝑇 ↔ 𝑠 ⊆ 𝑇 )
69 sseq1 ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ⊆ 𝑇 ↔ 𝑆 ⊆ 𝑇 ) )
70 68 69 bitrid ⊢ ( 𝑠 = 𝑆 → ( 𝑠 ∈ 𝒫 𝑇 ↔ 𝑆 ⊆ 𝑇 ) )
71 49 raleqdv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ↔ ∀ 𝑧 ∈ ( 𝑆 × 𝑆 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) )
72 fvex ⊢ ( 𝐻 ‘ 𝑧 ) ∈ V
73 72 elpw ⊢ ( ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ↔ ( 𝐻 ‘ 𝑧 ) ⊆ ( 𝐽 ‘ 𝑧 ) )
74 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐻 ‘ 𝑧 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
75 df-ov ⊢ ( 𝑥 𝐻 𝑦 ) = ( 𝐻 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
76 74 75 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐻 ‘ 𝑧 ) = ( 𝑥 𝐻 𝑦 ) )
77 fveq2 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐽 ‘ 𝑧 ) = ( 𝐽 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
78 df-ov ⊢ ( 𝑥 𝐽 𝑦 ) = ( 𝐽 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
79 77 78 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐽 ‘ 𝑧 ) = ( 𝑥 𝐽 𝑦 ) )
80 76 79 sseq12d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐻 ‘ 𝑧 ) ⊆ ( 𝐽 ‘ 𝑧 ) ↔ ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) )
81 73 80 bitrid ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ↔ ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) )
82 81 ralxp ⊢ ( ∀ 𝑧 ∈ ( 𝑆 × 𝑆 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) )
83 71 82 bitrdi ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) )
84 70 83 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑠 ∈ 𝒫 𝑇 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ↔ ( 𝑆 ⊆ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) ) )
85 84 ceqsexgv ⊢ ( 𝑆 ∈ V → ( ∃ 𝑠 ( 𝑠 = 𝑆 ∧ ( 𝑠 ∈ 𝒫 𝑇 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) ↔ ( 𝑆 ⊆ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) ) )
86 85 a1i ⊢ ( 𝜑 → ( 𝑆 ∈ V → ( ∃ 𝑠 ( 𝑠 = 𝑆 ∧ ( 𝑠 ∈ 𝒫 𝑇 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) ↔ ( 𝑆 ⊆ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) ) ) )
87 63 67 86 pm5.21ndd ⊢ ( 𝜑 → ( ∃ 𝑠 ( 𝑠 = 𝑆 ∧ ( 𝑠 ∈ 𝒫 𝑇 ∧ ∀ 𝑧 ∈ ( 𝑠 × 𝑠 ) ( 𝐻 ‘ 𝑧 ) ∈ 𝒫 ( 𝐽 ‘ 𝑧 ) ) ) ↔ ( 𝑆 ⊆ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) ) )
88 27 59 87 3bitrd ⊢ ( 𝜑 → ( 𝐻 ⊆cat 𝐽 ↔ ( 𝑆 ⊆ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) ) )